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.

1 files changed, 18 insertions, 47 deletions

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 ] \