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.

10 files changed, 41 insertions, 8 deletions

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