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.

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index f3800308b73e71cc55f00e78cde8abad7879907a..eeb9db5724da73c59863d1cd9a2afcfe3af702f1 100644 (file)
--- 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 b0a8444919c09397e4c24f14c7080f4d78752bbc..9b5af6dc45dc13bcd3f064ff4e47013247c3775e 100644 (file)
--- 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 4f760f57dad307943d41efc13ca5c43e4209751d..8b05c1dc74476ebf83f5136bbe712561c5ec2621 100644 (file)
--- 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 2736fd59b0125ce82a25b287a8d059e7c4d13d59..5a2295c4be8ea48c3953d6140abe50a361f83063 100644 (file)
--- 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 2d72325274d11abf9a9e99c7d4e2a54738e39da3..82737a0ac9fad6599f0609873a6b5d691ec46a7b 100644 (file)
--- 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 0e9d355239925186ab6615f3a9a0eb4fa5e6ce8e..08cb6f6a12733f898a673755a4b3133773e0a1fa 100644 (file)
--- 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 6596e42451874e14c1da134dd17153d24edabb57..f5447f95db700373325799ef7de6f186f4960e08 100644 (file)
--- 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 9a758602e5ede335b6a7d8a63f5f5f5035285c3e..bc12e44ba8f25d4e30817cd4c1b1b3d8834fd7b6 100644 (file)
--- 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 d220e299f8ab3609faccae428e3348b1dc79aee3..62aa5eeec8ef0472db585f0e00aeed866162f50d 100644 (file)
--- 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 29fd9fa05866f693ce46d3647962377cbf6694f0..1259459a202066c957641ad5a03621071825d112 100644 (file)
--- 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 47f20596129d616b55baa9a83121d58bb64f8095..be5b1eacbc4136529b788d951b126fa4b7ec3107 100644 (file)
--- 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 f0be2617ccac0a6a81230a00fc455f141f1664a0..f044c270635fc562595bb50aa563ba3594ba0ff7 100644 (file)
--- 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 cf6556375ab7a3c8a565c6216d8caa1a8921eff3..3e59cadc92e83474dbe6c631fb280a9b51dc18a5 100755 (executable)
--- 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 ] \