From 87bc1447d59e36410feab768ea2bbb577e58fb7b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 16 Apr 2021 13:06:40 +0200 Subject: [PATCH] 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. --- .github/workflows/ci.yml | 8 ++--- CMakeLists.txt | 1 + cmake/FindANTLR3.cmake | 15 ++++---- cmake/FindCLN.cmake | 1 + cmake/FindCaDiCaL.cmake | 1 + cmake/FindCryptoMiniSat.cmake | 1 + cmake/FindGMP.cmake | 1 + cmake/FindGTest.cmake | 1 + cmake/FindKissat.cmake | 1 + cmake/FindPoly.cmake | 1 + cmake/FindSymFPU.cmake | 7 ++-- cmake/deps-helper.cmake | 20 +++++++++++ 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 /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-