From: Gereon Kremer Date: Sat, 21 May 2022 22:14:45 +0000 (-0700) Subject: Add cross-compilation for arm64 on macOS (#8758) X-Git-Tag: cvc5-1.0.1~111 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4337cdb8e2a071ded73dbc9236c8bb2f4d42e6e5;p=cvc5.git Add cross-compilation for arm64 on macOS (#8758) Co-authored-by: Andres Noetzli --- diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 91832be57..ba2e2f602 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -29,6 +29,14 @@ jobs: exclude_regress: 3-4 run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump + - name: macos:production-arm64 + os: macos-11 + config: production --auto-download --python-bindings --editline --arm64 + cache-key: production-arm64 + strip-bin: strip + python-bindings: true + binary-name: cvc5-macOS-arm64 + - name: win64:production os: ubuntu-latest config: production --auto-download --win64 diff --git a/NEWS.md b/NEWS.md index f2910e9e1..fd4ae1b7f 100644 --- a/NEWS.md +++ b/NEWS.md @@ -3,6 +3,10 @@ This file contains a summary of important user-visible changes. cvc5 1.0.1 ========== +**New Features** + +- Support for cross-compiling an ARM binary of cvc5 on x86 macOS. + **Changes** - Removed support for non-standard `declare-funs`, `declare-consts`, and diff --git a/cmake/FindANTLR3.cmake b/cmake/FindANTLR3.cmake index f91286a69..a357ca909 100644 --- a/cmake/FindANTLR3.cmake +++ b/cmake/FindANTLR3.cmake @@ -103,6 +103,15 @@ if(NOT ANTLR3_FOUND_SYSTEM) unset(64bit) endif() + set(compilers "") + if (CMAKE_CROSSCOMPILING_MACOS) + # We set the CC and CXX flags as suggested in + # https://github.com/antlr/antlr3/blob/5c2a916a10139cdb5c7c8851ee592ed9c3b3d4ff/runtime/C/INSTALL#L133-L135. + set(compilers + "CC=${CMAKE_C_COMPILER} -arch ${CMAKE_OSX_ARCHITECTURES}" + "CXX=${CMAKE_CXX_COMPILER} -arch ${CMAKE_OSX_ARCHITECTURES}") + endif() + # Download, build and install antlr3 runtime ExternalProject_Add( ANTLR3-EP-runtime @@ -117,7 +126,9 @@ if(NOT ANTLR3_FOUND_SYSTEM) COMMAND ${CMAKE_COMMAND} -E copy /share/config.sub /config.sub - CONFIGURE_COMMAND /configure + CONFIGURE_COMMAND + /configure + ${compilers} --with-pic --disable-antlrdebug --disable-abiflags diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake index 5e94a7ee0..09523eb39 100644 --- a/cmake/FindCaDiCaL.cmake +++ b/cmake/FindCaDiCaL.cmake @@ -53,6 +53,10 @@ if(NOT CaDiCaL_FOUND_SYSTEM) # scripts unnecessarily fails for cross compilation thus we do the bare # minimum from the configure script here set(CXXFLAGS "-fPIC -O3 -DNDEBUG -DQUIET -std=c++11") + if(CMAKE_CROSSCOMPILING_MACOS) + set(CXXFLAGS "${CXXFLAGS} -arch ${CMAKE_OSX_ARCHITECTURES}") + endif() + # check for getc_unlocked check_symbol_exists("getc_unlocked" "cstdio" HAVE_UNLOCKED_IO) if(NOT HAVE_UNLOCKED_IO) diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake index 481bd973a..f63cf7c26 100644 --- a/cmake/FindGMP.cmake +++ b/cmake/FindGMP.cmake @@ -40,6 +40,16 @@ if(GMP_INCLUDE_DIR AND GMP_LIBRARIES) ) check_system_version("GMP") + + TRY_COMPILE(DOES_WORK "${DEPS_BASE}/try_compile/GMP-EP" + "${CMAKE_CURRENT_LIST_DIR}/deps-utils/gmp-test.cpp" + CMAKE_FLAGS -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE} + LINK_LIBRARIES gmpxx gmp + ) + if(NOT ${DOES_WORK}) + message(VERBOSE "System version for ${name} does not work in the selected configuration. Maybe we are cross-compiling?") + set(GMP_FOUND_SYSTEM FALSE) + endif() endif() if(NOT GMP_FOUND_SYSTEM) @@ -66,8 +76,16 @@ if(NOT GMP_FOUND_SYSTEM) endif() set(CONFIGURE_OPTS "") - if(CMAKE_CROSSCOMPILING) - set(CONFIGURE_OPTS --host=${TOOLCHAIN_PREFIX} --build=${CMAKE_HOST_SYSTEM_PROCESSOR}) + set(CONFIGURE_ENV "") + if(CMAKE_CROSSCOMPILING OR CMAKE_CROSSCOMPILING_MACOS) + set(CONFIGURE_OPTS + --host=${TOOLCHAIN_PREFIX} + --build=${CMAKE_HOST_SYSTEM_PROCESSOR}) + endif() + if (CMAKE_CROSSCOMPILING_MACOS) + set(CONFIGURE_ENV ${CMAKE_COMMAND} -E + env "CFLAGS=--target=${TOOLCHAIN_PREFIX}" + env "LDFLAGS=-arch ${CMAKE_OSX_ARCHITECTURES}") endif() # `CC_FOR_BUILD`, `--host`, and `--build` are passed to `configure` to ensure @@ -80,7 +98,7 @@ if(NOT GMP_FOUND_SYSTEM) URL https://gmplib.org/download/gmp/gmp-${GMP_VERSION}.tar.bz2 URL_HASH SHA1=2dcf34d4a432dbe6cce1475a835d20fe44f75822 CONFIGURE_COMMAND - ${CMAKE_COMMAND} -E env CC_FOR_BUILD=cc + ${CONFIGURE_ENV} /configure ${LINK_OPTS} --prefix= diff --git a/cmake/Toolchain-aarch64.cmake b/cmake/Toolchain-aarch64.cmake index cec586246..9e8423691 100644 --- a/cmake/Toolchain-aarch64.cmake +++ b/cmake/Toolchain-aarch64.cmake @@ -15,20 +15,34 @@ # Use: cmake .. -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-aarch64.cmake ## -SET(CMAKE_SYSTEM_NAME Linux) -SET(CMAKE_SYSTEM_PROCESSOR aarch64) +if(CMAKE_SYSTEM_NAME STREQUAL "Linux") -set(TOOLCHAIN_PREFIX aarch64-linux-gnu) + set(CMAKE_SYSTEM_NAME Linux) + set(CMAKE_SYSTEM_PROCESSOR aarch64) -SET(CMAKE_C_COMPILER ${TOOLCHAIN_PREFIX}-gcc) -SET(CMAKE_CXX_COMPILER ${TOOLCHAIN_PREFIX}-g++) + set(TOOLCHAIN_PREFIX aarch64-linux-gnu) -# Set target environment path -SET(CMAKE_FIND_ROOT_PATH /usr/${TOOLCHAIN_PREFIX}) + set(CMAKE_C_COMPILER ${TOOLCHAIN_PREFIX}-gcc) + set(CMAKE_CXX_COMPILER ${TOOLCHAIN_PREFIX}-g++) -# Adjust the default behaviour of the find_XXX() commands: -# search headers and libraries in the target environment, search -# programs in the host environment -set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM NEVER) -set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY ONLY) -set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY) + # Set target environment path + set(CMAKE_FIND_ROOT_PATH /usr/${TOOLCHAIN_PREFIX}) + + # Adjust the default behaviour of the find_XXX() commands: + # search headers and libraries in the target environment, search + # programs in the host environment + set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM NEVER) + set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY ONLY) + set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY) + +elseif(CMAKE_SYSTEM_NAME STREQUAL "Darwin") + + set(CMAKE_SYSTEM_NAME Darwin) + set(CMAKE_SYSTEM_PROCESSOR arm64) + + set(TOOLCHAIN_PREFIX arm64-apple-darwin) + + set(CMAKE_CROSSCOMPILING_MACOS TRUE) + set(CMAKE_OSX_ARCHITECTURES arm64 CACHE INTERNAL "") + +endif() diff --git a/cmake/deps-utils/gmp-test.cpp b/cmake/deps-utils/gmp-test.cpp new file mode 100644 index 000000000..88d1ca62c --- /dev/null +++ b/cmake/deps-utils/gmp-test.cpp @@ -0,0 +1,7 @@ +#include + +int main() +{ + mpz_class i = 0; + return 0; +}