diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-04-16 13:06:40 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-16 11:06:40 +0000 |
commit | 87bc1447d59e36410feab768ea2bbb577e58fb7b (patch) | |
tree | f4b53d672c94eb538e07193a1fcd7134767773d6 | |
parent | 7cae3947227391313d93fa1e2ef7bfb4e9e3986d (diff) |
Refactor cmake: auto-download and default-on dependencies (#6355)
This PR changes a few things in how dependencies are handled during configuration:
- --x-dir are removed for most dependencies, use the generic --dep-path instead
- the cmake ENABLE_AUTO_DOWNLOAD determines whether we attempt to download missing dependencies ourselves
- external projects check this option and send an error if it is OFF
- some optional dependencies are enabled by default (CaDiCaL, Poly, SymFPU)
This will essentially fail every call to ./configure.sh until the user specifies --auto-download.
-rw-r--r-- | .github/workflows/ci.yml | 8 | ||||
-rw-r--r-- | CMakeLists.txt | 1 | ||||
-rw-r--r-- | cmake/FindANTLR3.cmake | 15 | ||||
-rw-r--r-- | cmake/FindCLN.cmake | 1 | ||||
-rw-r--r-- | cmake/FindCaDiCaL.cmake | 1 | ||||
-rw-r--r-- | cmake/FindCryptoMiniSat.cmake | 1 | ||||
-rw-r--r-- | cmake/FindGMP.cmake | 1 | ||||
-rw-r--r-- | cmake/FindGTest.cmake | 1 | ||||
-rw-r--r-- | cmake/FindKissat.cmake | 1 | ||||
-rw-r--r-- | cmake/FindPoly.cmake | 1 | ||||
-rw-r--r-- | cmake/FindSymFPU.cmake | 7 | ||||
-rw-r--r-- | cmake/deps-helper.cmake | 20 | ||||
-rwxr-xr-x | configure.sh | 65 |
13 files changed, 64 insertions, 59 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f3800308b..eeb9db572 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -23,7 +23,7 @@ jobs: include: - name: production - config: production --all-bindings --editline --poly --symfpu + config: production --auto-download --all-bindings --editline cache-key: production python-bindings: true check-examples: true @@ -31,7 +31,7 @@ jobs: run_regression_args: --no-check-unsat-cores --no-check-proofs - name: production-clang - config: production + config: production --auto-download cache-key: productionclang check-examples: true env: CC=clang CXX=clang++ @@ -40,14 +40,14 @@ jobs: run_regression_args: --no-check-unsat-cores --no-check-proofs - name: production-dbg - config: production --assertions --tracing --unit-testing --symfpu --editline + config: production --auto-download --assertions --tracing --unit-testing --editline cache-key: dbg os: ubuntu-latest exclude_regress: 3-4 run_regression_args: --no-check-unsat-cores - name: production-dbg-clang - config: production --assertions --tracing --unit-testing --symfpu --cln --gpl --poly + config: production --auto-download --assertions --tracing --unit-testing --cln --gpl cache-key: dbgclang env: CC=clang CXX=clang++ os: ubuntu-latest diff --git a/CMakeLists.txt b/CMakeLists.txt index b0a844491..9b5af6dc4 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -104,6 +104,7 @@ cvc4_option(ENABLE_VALGRIND "Enable valgrind instrumentation") cvc4_option(ENABLE_SHARED "Build as shared library") cvc4_option(ENABLE_STATIC_BINARY "Build static binaries with statically linked system libraries") +cvc4_option(ENABLE_AUTO_DOWNLOAD "Enable automatic download of dependencies") # >> 2-valued: ON OFF # > for options where we don't need to detect if set by user (default: OFF) option(ENABLE_BEST "Enable dependencies known to give best performance") diff --git a/cmake/FindANTLR3.cmake b/cmake/FindANTLR3.cmake index 4f760f57d..8b05c1dc7 100644 --- a/cmake/FindANTLR3.cmake +++ b/cmake/FindANTLR3.cmake @@ -18,12 +18,12 @@ include(deps-helper) -find_program(ANTLR3_BINARY NAMES antlr3) +find_file(ANTLR3_JAR NAMES antlr-3.4-complete.jar PATH_SUFFIXES share/java/) find_path(ANTLR3_INCLUDE_DIR NAMES antlr3.h) find_library(ANTLR3_RUNTIME NAMES antlr3c) set(ANTLR3_FOUND_SYSTEM FALSE) -if(ANTLR3_BINARY AND ANTLR3_INCLUDE_DIR AND ANTLR3_RUNTIME) +if(ANTLR3_JAR AND ANTLR3_INCLUDE_DIR AND ANTLR3_RUNTIME) set(ANTLR3_FOUND_SYSTEM TRUE) # Parse ANTLR3 version @@ -34,6 +34,7 @@ if(ANTLR3_BINARY AND ANTLR3_INCLUDE_DIR AND ANTLR3_RUNTIME) endif() if(NOT ANTLR3_FOUND_SYSTEM) + check_auto_download("ANTLR3" "") include(ExternalProject) set(ANTLR3_VERSION "3.4") @@ -96,18 +97,20 @@ if(NOT ANTLR3_FOUND_SYSTEM) BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libantlr3c.a ) - find_package(Java COMPONENTS Runtime REQUIRED) - set(ANTLR3_BINARY ${Java_JAVA_EXECUTABLE} - -cp "${DEPS_BASE}/share/java/antlr-3.4-complete.jar" org.antlr.Tool) + set(ANTLR3_JAR "${DEPS_BASE}/share/java/antlr-3.4-complete.jar") set(ANTLR3_INCLUDE_DIR "${DEPS_BASE}/include/") set(ANTLR3_RUNTIME "${DEPS_BASE}/lib/libantlr3c.a") endif() +find_package(Java COMPONENTS Runtime REQUIRED) + set(ANTLR3_FOUND TRUE) # This may not be a single binary: the EP has a whole commandline # We thus do not make this an executable target. # Just call ${ANTLR3_COMMAND} instead. -set(ANTLR3_COMMAND ${ANTLR3_BINARY} CACHE STRING "run ANTLR3" FORCE) +set(ANTLR3_COMMAND ${Java_JAVA_EXECUTABLE} -cp + "${DEPS_BASE}/share/java/antlr-3.4-complete.jar" org.antlr.Tool + CACHE STRING "run ANTLR3" FORCE) add_library(ANTLR3 STATIC IMPORTED GLOBAL) set_target_properties(ANTLR3 PROPERTIES IMPORTED_LOCATION "${ANTLR3_RUNTIME}") diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake index 2736fd59b..5a2295c4b 100644 --- a/cmake/FindCLN.cmake +++ b/cmake/FindCLN.cmake @@ -34,6 +34,7 @@ if(CLN_INCLUDE_DIR AND CLN_LIBRARIES) endif() if(NOT CLN_FOUND_SYSTEM) + check_auto_download("CLN" "--no-cln") include(ExternalProject) fail_if_cross_compiling("Windows" "" "CLN" "autoconf fails") diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake index 2d7232527..82737a0ac 100644 --- a/cmake/FindCaDiCaL.cmake +++ b/cmake/FindCaDiCaL.cmake @@ -39,6 +39,7 @@ if(CaDiCaL_INCLUDE_DIR AND CaDiCaL_LIBRARIES) endif() if(NOT CaDiCaL_FOUND_SYSTEM) + check_auto_download("CaDiCaL" "--no-cadical") include(CheckSymbolExists) include(ExternalProject) diff --git a/cmake/FindCryptoMiniSat.cmake b/cmake/FindCryptoMiniSat.cmake index 0e9d35523..08cb6f6a1 100644 --- a/cmake/FindCryptoMiniSat.cmake +++ b/cmake/FindCryptoMiniSat.cmake @@ -35,6 +35,7 @@ if(cryptominisat5_FOUND) endif() if(NOT CryptoMiniSat_FOUND_SYSTEM) + check_auto_download("CryptoMiniSat" "--no-cryptominisat") include(ExternalProject) set(CryptoMiniSat_VERSION "5.8.0") diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake index 6596e4245..f5447f95d 100644 --- a/cmake/FindGMP.cmake +++ b/cmake/FindGMP.cmake @@ -43,6 +43,7 @@ if(GMP_INCLUDE_DIR AND GMP_LIBRARIES) endif() if(NOT GMP_FOUND_SYSTEM) + check_auto_download("GMP" "") include(ExternalProject) set(GMP_VERSION "6.2.1") diff --git a/cmake/FindGTest.cmake b/cmake/FindGTest.cmake index 9a758602e..bc12e44ba 100644 --- a/cmake/FindGTest.cmake +++ b/cmake/FindGTest.cmake @@ -25,6 +25,7 @@ if(GTest_INCLUDE_DIR AND GTest_LIBRARIES AND GTest_MAIN_LIBRARIES) endif() if(NOT GTest_FOUND_SYSTEM) + check_auto_download("GTest" "") include(ExternalProject) set(GTest_VERSION "1.10.0") diff --git a/cmake/FindKissat.cmake b/cmake/FindKissat.cmake index d220e299f..62aa5eeec 100644 --- a/cmake/FindKissat.cmake +++ b/cmake/FindKissat.cmake @@ -39,6 +39,7 @@ if(Kissat_INCLUDE_DIR AND Kissat_LIBRARIES) endif() if(NOT Kissat_FOUND_SYSTEM) + check_auto_download("Kissat" "--no-kissat") include(ExternalProject) fail_if_include_missing("sys/resource.h" "Kissat") diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake index 29fd9fa05..1259459a2 100644 --- a/cmake/FindPoly.cmake +++ b/cmake/FindPoly.cmake @@ -38,6 +38,7 @@ if(Poly_INCLUDE_DIR endif() if(NOT Poly_FOUND_SYSTEM) + check_auto_download("Poly" "--no-poly") include(ExternalProject) set(Poly_VERSION "0.1.9") diff --git a/cmake/FindSymFPU.cmake b/cmake/FindSymFPU.cmake index 47f205961..be5b1eacb 100644 --- a/cmake/FindSymFPU.cmake +++ b/cmake/FindSymFPU.cmake @@ -17,11 +17,14 @@ find_path(SymFPU_INCLUDE_DIR NAMES symfpu/core/unpackedFloat.h) +set(SymFPU_FOUND_SYSTEM FALSE) if(SymFPU_INCLUDE_DIR) # Found SymFPU to be installed system-wide set(SymFPU_FOUND_SYSTEM TRUE) -else() - set(SymFPU_FOUND_SYSTEM FALSE) +endif() + +if(NOT SymFPU_FOUND_SYSTEM) + check_auto_download("SymFPU" "--no-symfpu") include(ExternalProject) include(deps-helper) diff --git a/cmake/deps-helper.cmake b/cmake/deps-helper.cmake index f0be2617c..f044c2706 100644 --- a/cmake/deps-helper.cmake +++ b/cmake/deps-helper.cmake @@ -39,6 +39,26 @@ if(CMAKE_VERSION VERSION_GREATER_EQUAL "3.14") ) endif() +macro(check_auto_download name disable_option) + if(NOT ENABLE_AUTO_DOWNLOAD) + if (${name}_FIND_VERSION) + set(depname "${name} (>= ${${name}_FIND_VERSION})") + else() + set(depname "${name}") + endif() + if("${disable_option}" STREQUAL "") + message(FATAL_ERROR "Could not find the required dependency +${depname} in the system. Please install it yourself or use --auto-download to \ +let us download and build it for you.") + else() + message(FATAL_ERROR "Could not find the optional dependency +${depname} in the system. You can disable this dependency with \ +${disable_option}, install it yourself or use --auto-download to let us \ +download and build it for you.") + endif() + endif() +endmacro(check_auto_download) + macro(check_system_version name) # find_package sets this variable when called with a version # https://cmake.org/cmake/help/latest/command/find_package.html#version-selection diff --git a/configure.sh b/configure.sh index cf6556375..3e59cadc9 100755 --- a/configure.sh +++ b/configure.sh @@ -33,6 +33,7 @@ The following flags enable optional features (disable with --no-<option name>). --static build static libraries and binaries [default=no] --static-binary statically link against system libraries (must be disabled for static macOS builds) [default=yes] + --auto-download automatically download dependencies if necessary --debug-symbols include debug symbols --valgrind Valgrind instrumentation --debug-context-mm use the debug context memory manager @@ -58,22 +59,17 @@ The following flags enable optional packages (disable with --no-<option name>). --cln use CLN instead of GMP --glpk use GLPK simplex solver --abc use the ABC AIG library - --cadical use the CaDiCaL SAT solver + --cadical use the CaDiCaL SAT solver [default=yes] --cryptominisat use the CryptoMiniSat SAT solver --kissat use the Kissat SAT solver - --poly use the LibPoly library - --symfpu use SymFPU for floating point solver + --poly use the LibPoly library [default=yes] + --symfpu use SymFPU for floating point solver [default=yes] --editline support the editline library Optional Path to Optional Packages: --abc-dir=PATH path to top level of ABC source tree - --cadical-dir=PATH path to top level of CaDiCaL source tree - --cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree --glpk-dir=PATH path to top level of GLPK installation - --gmp-dir=PATH path to top level of GMP installation - --kissat-dir=PATH path to top level of Kissat source tree - --poly-dir=PATH path to top level of LibPoly source tree - --symfpu-dir=PATH path to top level of SymFPU source tree + --dep-path=PATH path to a dependency installation dir Build limitations: --lib-only only build the library, but not the executable or @@ -111,7 +107,8 @@ buildtype=default abc=default asan=default assertions=default -cadical=default +auto_download=default +cadical=ON cln=default comp_inc=default coverage=default @@ -123,7 +120,7 @@ dumping=default glpk=default gpl=default kissat=default -poly=default +poly=ON muzzle=default ninja=default profiling=default @@ -134,7 +131,7 @@ editline=default shared=default static_binary=default statistics=default -symfpu=default +symfpu=ON tracing=default tsan=default ubsan=default @@ -145,13 +142,7 @@ arm64=default werror=default abc_dir=default -cadical_dir=default -cryptominisat_dir=default glpk_dir=default -gmp_dir=default -kissat_dir=default -poly_dir=default -symfpu_dir=default lib_only=default @@ -258,6 +249,9 @@ do --static-binary) static_binary=ON;; --no-static-binary) static_binary=OFF;; + --auto-download) auto_download=ON;; + --no-auto-download) auto_download=OFF;; + --statistics) statistics=ON;; --no-statistics) statistics=OFF;; @@ -295,26 +289,11 @@ do --abc-dir) die "missing argument to $1 (try -h)" ;; --abc-dir=*) abc_dir=${1##*=} ;; - --cadical-dir) die "missing argument to $1 (try -h)" ;; - --cadical-dir=*) cadical_dir=${1##*=} ;; - - --cryptominisat-dir) die "missing argument to $1 (try -h)" ;; - --cryptominisat-dir=*) cryptominisat_dir=${1##*=} ;; - --glpk-dir) die "missing argument to $1 (try -h)" ;; --glpk-dir=*) glpk_dir=${1##*=} ;; - --gmp-dir) die "missing argument to $1 (try -h)" ;; - --gmp-dir=*) gmp_dir=${1##*=} ;; - - --kissat-dir) die "missing argument to $1 (try -h)" ;; - --kissat-dir=*) kissat_dir=${1##*=} ;; - - --poly-dir) die "missing argument to $1 (try -h)" ;; - --poly-dir=*) poly_dir=${1##*=} ;; - - --symfpu-dir) die "missing argument to $1 (try -h)" ;; - --symfpu-dir=*) symfpu_dir=${1##*=} ;; + --dep-path) die "missing argument to $1 (try -h)" ;; + --dep-path=*) dep_path="${dep_path};${1##*=}" ;; --lib-only) lib_only=ON ;; @@ -347,6 +326,8 @@ cmake_opts="" [ $asan != default ] \ && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan" +[ $auto_download != default ] \ + && cmake_opts="$cmake_opts -DENABLE_AUTO_DOWNLOAD=$auto_download" [ $ubsan != default ] \ && cmake_opts="$cmake_opts -DENABLE_UBSAN=$ubsan" [ $tsan != default ] \ @@ -414,20 +395,10 @@ cmake_opts="" && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu" [ "$abc_dir" != default ] \ && cmake_opts="$cmake_opts -DABC_DIR=$abc_dir" -[ "$cadical_dir" != default ] \ - && cmake_opts="$cmake_opts -DCADICAL_DIR=$cadical_dir" -[ "$cryptominisat_dir" != default ] \ - && cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir" [ "$glpk_dir" != default ] \ && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir" -[ "$gmp_dir" != default ] \ - && cmake_opts="$cmake_opts -DGMP_DIR=$gmp_dir" -[ "$kissat_dir" != default ] \ - && cmake_opts="$cmake_opts -DKISSAT=$kissat_dir" -[ "$poly_dir" != default ] \ - && cmake_opts="$cmake_opts -DPOLY_DIR=$poly_dir" -[ "$symfpu_dir" != default ] \ - && cmake_opts="$cmake_opts -DSYMFPU_DIR=$symfpu_dir" +[ "$dep_path" != default ] \ + && cmake_opts="$cmake_opts -DCMAKE_PREFIX_PATH=$dep_path" [ "$lib_only" != default ] \ && cmake_opts="$cmake_opts -DBUILD_LIB_ONLY=$lib_only" [ "$install_prefix" != default ] \ |