Combine `--static` and `--static-binary` (#7520)

This PR combines the two configure flags --static and --static-binary into a single --static. Consequently, the two corresponding cmake variables are combined as well. The two variables have been implying each other for some time now and were only used to build not-completely-static binaries for MacOS, which is now done automatically anyway.

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 82916f26b4187fe8389ca91442ccf20558f0d3f0..1acc26c5a04aa9fc638ce804e21785b2bffc496e 100644 (file)
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -8,7 +8,7 @@ jobs:
         include:
           - name: ubuntu:production
             os: ubuntu-latest
-            config: production --auto-download --all-bindings --editline --docs --static-binary
+            config: production --auto-download --all-bindings --editline --docs --static
             cache-key: production
             python-bindings: true
             build-documentation: true
@@ -19,7 +19,7 @@ jobs:
 
           - name: macos:production
             os: macos-11
-            config: production --auto-download --all-bindings --editline --static-binary
+            config: production --auto-download --all-bindings --editline --static
             cache-key: production
             python-bindings: true
             check-examples: true

diff --git a/CMakeLists.txt b/CMakeLists.txt
index f5abf6ea6b4e5b8e67e7cbfa80d05af1e8ed8048..1afb2cfc8bb2c0741d93d3e9610ace7d910fb175 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -86,9 +86,7 @@ cvc5_option(ENABLE_STATISTICS     "Enable statistics")
 cvc5_option(ENABLE_TRACING        "Enable tracing")
 cvc5_option(ENABLE_UNIT_TESTING   "Enable unit testing")
 cvc5_option(ENABLE_VALGRIND       "Enable valgrind instrumentation")
-cvc5_option(ENABLE_STATIC_LIBRARY "Enable building static library")
-cvc5_option(ENABLE_STATIC_BINARY
-            "Build static binaries with statically linked system libraries")
+cvc5_option(ENABLE_STATIC_BUILD   "Enable building static libraries and binary")
 cvc5_option(ENABLE_AUTO_DOWNLOAD  "Enable automatic download of dependencies")
 cvc5_option(ENABLE_IPO            "Enable interprocedural optimization")
 # >> 2-valued: ON OFF
@@ -224,18 +222,6 @@ if(ENABLE_IPO)
   set(CMAKE_INTERPROCEDURAL_OPTIMIZATION TRUE)
 endif()
 
-
-#-----------------------------------------------------------------------------#
-# Option defaults (three-valued options (cvc5_option(...)))
-#
-# These options are only set if their value is IGNORE. Otherwise, the user
-# already set the option, which we don't want to overwrite.
-
-if(ENABLE_STATIC_BINARY)
-  message(STATUS "Enable static library for static binary build.")
-  cvc5_set_option(ENABLE_STATIC_LIBRARY ON)
-endif()
-
 #-----------------------------------------------------------------------------#
 
 # Only enable unit testing if assertions are enabled. Otherwise, unit tests
@@ -463,7 +449,7 @@ include(IWYU)
 #-----------------------------------------------------------------------------#
 
 include(ConfigureCvc5)
-if(ENABLE_STATIC_BINARY)
+if(ENABLE_STATIC_BUILD)
   set(CVC5_STATIC_BUILD ON)
 endif()
 
@@ -504,7 +490,7 @@ include(CMakePackageConfigHelpers)
 # (in the assumption that only reasonably experienced users use this and
 # also that custom installation prefixes are not used for longer periods of
 # time anyway). Also, we print a big warning with further instructions.
-if(NOT ENABLE_STATIC_BINARY)
+if(NOT ENABLE_STATIC_BUILD)
   # Get the libraries that cvc5 links against
   get_target_property(libs cvc5-shared INTERFACE_LINK_LIBRARIES)
   set(LIBS_SHARED_FROM_DEPS "")
@@ -615,8 +601,7 @@ print_config("Profiling (gprof)         " ${ENABLE_PROFILING})
 print_config("Unit tests                " ${ENABLE_UNIT_TESTING})
 print_config("Valgrind                  " ${ENABLE_VALGRIND})
 message("")
-print_config("Static library            " ${ENABLE_STATIC_LIBRARY})
-print_config("Static binary             " ${ENABLE_STATIC_BINARY})
+print_config("Static build              " ${ENABLE_STATIC_BUILD})
 print_config("Python bindings           " ${BUILD_BINDINGS_PYTHON})
 print_config("Java bindings             " ${BUILD_BINDINGS_JAVA})
 print_config("Python2                   " ${USE_PYTHON2})

diff --git a/INSTALL.rst b/INSTALL.rst
index 7df21cb4cf18cec71bb8875e5d0cc5dcb134acd8..8c2b6731575a1c7483b2975bb0d8cb09c929b274 100644 (file)
--- a/INSTALL.rst
+++ b/INSTALL.rst
@@ -33,7 +33,7 @@ dependencies.  We also have a Homebrew Tap available at
 https://github.com/CVC4/homebrew-cvc4 .
 Note that linking system libraries statically is
 `strongly discouraged <https://developer.apple.com/library/archive/qa/qa1118/_index.html>`_
-on macOS. Using ``./configure.sh --static-binary`` will thus produce a binary
+on macOS. Using ``./configure.sh --static`` will thus produce a binary
 that uses static versions of all our dependencies, but is still a dynamically
 linked binary.
 
@@ -45,7 +45,7 @@ Cross-compiling cvc5 with Mingw-w64 can be done as follows:
 
 .. code:: bash
 
-  ./configure.sh --win64 --static-binary <configure options...>
+  ./configure.sh --win64 --static <configure options...>
 
   cd <build_dir>   # default is ./build
   make             # use -jN for parallel build with N threads
@@ -431,6 +431,6 @@ linked LGPL libraries perform the following steps:
 
 .. code::
   
-  ./configure.sh --static-binary <options>
+  ./configure.sh --static <options>
 
 7. Follow remaining steps from `build instructions <#building-cvc5>`_

diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake
index 2b17d8073fc24ee0403581f8d32abdfa2c0fc2c2..e479c15d05f622126eac9aaf6cb951a878065e4f 100644 (file)
--- a/cmake/ConfigCompetition.cmake
+++ b/cmake/ConfigCompetition.cmake
@@ -32,7 +32,7 @@ cvc5_set_option(ENABLE_DUMPING OFF)
 # enable_muzzle=yes
 cvc5_set_option(ENABLE_MUZZLE ON)
 # enable_valgrind=no
-cvc5_set_option(ENABLE_STATIC_BINARY ON)
+cvc5_set_option(ENABLE_STATIC_BUILD ON)
 cvc5_set_option(ENABLE_UNIT_TESTING OFF)
 
 # By default, we include all dependencies in our competition build that are

diff --git a/cmake/FindANTLR3.cmake b/cmake/FindANTLR3.cmake
index e389e15f0107626addae39604997e3755e93ba18..bc4afda235a6c384ccb5d9e87b3242d2372ec014 100644 (file)
--- a/cmake/FindANTLR3.cmake
+++ b/cmake/FindANTLR3.cmake
@@ -33,7 +33,7 @@ if(ANTLR3_JAR AND ANTLR3_INCLUDE_DIR AND ANTLR3_LIBRARIES)
     check_system_version("ANTLR3")
 endif()
 
-if(ENABLE_STATIC_LIBRARY AND ANTLR3_FOUND_SYSTEM)
+if(ENABLE_STATIC_BUILD AND ANTLR3_FOUND_SYSTEM)
   force_static_library()
   find_library(ANTLR3_STATIC_LIBRARIES NAMES antlr3c)
   if(NOT ANTLR3_STATIC_LIBRARIES)

diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake
index 11bf8ed98a8bc29013c9a3613256b143b6a62d74..3f83b61e26343810ede30780bb5e83c265f71f3b 100644 (file)
--- a/cmake/FindCLN.cmake
+++ b/cmake/FindCLN.cmake
@@ -33,7 +33,7 @@ if(CLN_INCLUDE_DIR AND CLN_LIBRARIES)
   check_system_version("CLN")
 endif()
 
-if(ENABLE_STATIC_LIBRARY AND CLN_FOUND_SYSTEM)
+if(ENABLE_STATIC_BUILD AND CLN_FOUND_SYSTEM)
   force_static_library()
   find_library(CLN_STATIC_LIBRARIES NAMES cln)
   if(NOT CLN_STATIC_LIBRARIES)
@@ -94,7 +94,7 @@ set_target_properties(CLN_SHARED PROPERTIES
 target_link_libraries(CLN_SHARED INTERFACE GMP_SHARED)
 
 
-if(ENABLE_STATIC_LIBRARY)
+if(ENABLE_STATIC_BUILD)
   add_library(CLN_STATIC STATIC IMPORTED GLOBAL)
   set_target_properties(CLN_STATIC PROPERTIES
     IMPORTED_LOCATION "${CLN_STATIC_LIBRARIES}"

diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake
index 5a849153ba637cc7ab6839b491487410bd9312da..bea0e1bf169d12357b4642505496842f178d3157 100644 (file)
--- a/cmake/FindGMP.cmake
+++ b/cmake/FindGMP.cmake
@@ -42,7 +42,7 @@ if(GMP_INCLUDE_DIR AND GMP_LIBRARIES)
   check_system_version("GMP")
 endif()
 
-if(ENABLE_STATIC_LIBRARY AND GMP_FOUND_SYSTEM)
+if(ENABLE_STATIC_BUILD AND GMP_FOUND_SYSTEM)
   force_static_library()
   find_library(GMP_STATIC_LIBRARIES NAMES gmp)
   if(NOT GMP_STATIC_LIBRARIES)
@@ -132,7 +132,7 @@ if(CMAKE_SYSTEM_NAME STREQUAL "Windows")
   set_target_properties(GMP_SHARED PROPERTIES IMPORTED_IMPLIB "${GMP_LIBRARIES}")
 endif()
 
-if(ENABLE_STATIC_LIBRARY)
+if(ENABLE_STATIC_BUILD)
   add_library(GMP_STATIC STATIC IMPORTED GLOBAL)
   set_target_properties(GMP_STATIC PROPERTIES
     IMPORTED_LOCATION "${GMP_STATIC_LIBRARIES}"
@@ -150,7 +150,7 @@ if(GMP_FOUND_SYSTEM)
 else()
   message(STATUS "Building GMP ${GMP_VERSION}: ${GMP_LIBRARIES}")
   add_dependencies(GMP_SHARED GMP-EP)
-  if(ENABLE_STATIC_LIBRARY)
+  if(ENABLE_STATIC_BUILD)
     add_dependencies(GMP_STATIC GMP-EP)
   endif()
 endif()

diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake
index f363147cc9e3ebc75a6fca005d62a6e706e3a6ad..e19e1c57d05badbee22f7363759dd80c5c6a826b 100644 (file)
--- a/cmake/FindPoly.cmake
+++ b/cmake/FindPoly.cmake
@@ -37,7 +37,7 @@ if(Poly_INCLUDE_DIR
   check_system_version("Poly")
 endif()
 
-if(ENABLE_STATIC_LIBRARY AND Poly_FOUND_SYSTEM)
+if(ENABLE_STATIC_BUILD AND Poly_FOUND_SYSTEM)
   force_static_library()
   find_library(Poly_STATIC_LIBRARIES NAMES poly)
   find_library(PolyXX_STATIC_LIBRARIES NAMES polyxx)
@@ -158,7 +158,7 @@ if(CMAKE_SYSTEM_NAME STREQUAL "Windows")
   set_target_properties(Polyxx_SHARED PROPERTIES IMPORTED_IMPLIB "${PolyXX_LIBRARIES}")
 endif()
 
-if(ENABLE_STATIC_LIBRARY)
+if(ENABLE_STATIC_BUILD)
   add_library(Poly_STATIC STATIC IMPORTED GLOBAL)
   set_target_properties(Poly_STATIC PROPERTIES
     IMPORTED_LOCATION "${Poly_STATIC_LIBRARIES}"
@@ -194,7 +194,7 @@ else()
     DESTINATION ${CMAKE_INSTALL_LIBDIR}
   )
 
-  if(ENABLE_STATIC_LIBRARY)
+  if(ENABLE_STATIC_BUILD)
     add_dependencies(Poly_STATIC Poly-EP)
     add_dependencies(Polyxx_STATIC Poly-EP)
   endif()

diff --git a/configure.sh b/configure.sh
index a8bf19b7939d52bcb69ad3175185188baf53f5dc..641be5c18f4db476d4025e308ceb807e344c53fc 100755 (executable)
--- a/configure.sh
+++ b/configure.sh
@@ -31,8 +31,6 @@ General options;
 Features:
 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
@@ -131,8 +129,7 @@ python2=default
 python_bindings=default
 java_bindings=default
 editline=default
-static_library=default
-static_binary=default
+static=default
 statistics=default
 tracing=default
 tsan=default
@@ -249,11 +246,8 @@ do
     --muzzle) muzzle=ON;;
     --no-muzzle) muzzle=OFF;;
 
-    --static) static_library=ON; static_binary=ON;;
-    --no-static) static_library=OFF;;
-
-    --static-binary) static_binary=ON;;
-    --no-static-binary) static_binary=OFF;;
+    --static) static=ON;;
+    --no-static) static=OFF;;
 
     --auto-download) auto_download=ON;;
     --no-auto-download) auto_download=OFF;;
@@ -356,10 +350,8 @@ fi
 [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
 [ $muzzle != default ] \
   && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
-[ $static_library != default ] \
-  && cmake_opts="$cmake_opts -DENABLE_STATIC_LIBRARY=$static_library"
-[ $static_binary != default ] \
-  && cmake_opts="$cmake_opts -DENABLE_STATIC_BINARY=$static_binary"
+[ $static != default ] \
+  && cmake_opts="$cmake_opts -DENABLE_STATIC_BUILD=$static"
 [ $statistics != default ] \
   && cmake_opts="$cmake_opts -DENABLE_STATISTICS=$statistics"
 [ $tracing != default ] \

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2cb3457e18248aa9c9c47ef72b96c8b0bf67eef1..201ab6eb27cce05713cef316bf16b0912b88a1ed 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1339,7 +1339,7 @@ install(TARGETS cvc5-shared
   ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}
 )
 
-if(ENABLE_STATIC_LIBRARY)
+if(ENABLE_STATIC_BUILD)
   add_library(cvc5-static STATIC $<TARGET_OBJECTS:cvc5-obj> $<TARGET_OBJECTS:cvc5base> $<TARGET_OBJECTS:cvc5context>)
   set_target_properties(cvc5-static PROPERTIES OUTPUT_NAME cvc5)
   target_include_directories(cvc5-static
@@ -1360,7 +1360,7 @@ generate_export_header(cvc5-obj BASE_NAME cvc5)
 add_dependencies(cvc5-obj GMP_SHARED)
 target_include_directories(cvc5-obj PRIVATE ${GMP_INCLUDE_DIR})
 target_link_libraries(cvc5-shared PRIVATE GMP_SHARED)
-if(ENABLE_STATIC_LIBRARY)
+if(ENABLE_STATIC_BUILD)
   target_link_libraries(cvc5-static PUBLIC GMP_STATIC)
 endif()
 
@@ -1368,7 +1368,7 @@ endif()
 # Note: For glibc < 2.17 we have to additionally link against rt (man clock_gettime).
 #       RT_LIBRARIES should be empty for glibc >= 2.17
 target_link_libraries(cvc5-shared PRIVATE ${RT_LIBRARIES})
-if(ENABLE_STATIC_LIBRARY)
+if(ENABLE_STATIC_BUILD)
   target_link_libraries(cvc5-static PRIVATE ${RT_LIBRARIES})
 endif()
 
@@ -1383,7 +1383,7 @@ endif()
 add_dependencies(cvc5-obj CaDiCaL)
 target_include_directories(cvc5-obj PRIVATE ${CaDiCaL_INCLUDE_DIR})
 target_link_libraries(cvc5-shared PRIVATE CaDiCaL)
-if(ENABLE_STATIC_LIBRARY)
+if(ENABLE_STATIC_BUILD)
   target_link_libraries(cvc5-static PUBLIC CaDiCaL)
 endif()
 
@@ -1391,7 +1391,7 @@ if(USE_CLN)
   add_dependencies(cvc5-obj CLN_SHARED)
   target_include_directories(cvc5-obj PRIVATE ${CLN_INCLUDE_DIR})
   target_link_libraries(cvc5-shared PRIVATE CLN_SHARED)
-  if(ENABLE_STATIC_LIBRARY)
+  if(ENABLE_STATIC_BUILD)
     target_link_libraries(cvc5-static PUBLIC CLN_STATIC)
   endif()
 endif()
@@ -1399,7 +1399,7 @@ if(USE_CRYPTOMINISAT)
   add_dependencies(cvc5-obj CryptoMiniSat)
   target_include_directories(cvc5-obj PRIVATE ${CryptoMiniSat_INCLUDE_DIR})
   target_link_libraries(cvc5-shared PRIVATE CryptoMiniSat)
-  if(ENABLE_STATIC_LIBRARY)
+  if(ENABLE_STATIC_BUILD)
     target_link_libraries(cvc5-static PUBLIC CryptoMiniSat)
   endif()
 endif()
@@ -1407,14 +1407,14 @@ if(USE_KISSAT)
   add_dependencies(cvc5-obj Kissat)
   target_include_directories(cvc5-obj PRIVATE ${Kissat_INCLUDE_DIR})
   target_link_libraries(cvc5-shared PRIVATE Kissat)
-  if(ENABLE_STATIC_LIBRARY)
+  if(ENABLE_STATIC_BUILD)
     target_link_libraries(cvc5-static PUBLIC Kissat)
   endif()
 endif()
 if(USE_GLPK)
   target_include_directories(cvc5-obj PRIVATE ${GLPK_INCLUDE_DIR})
   target_link_libraries(cvc5-shared PRIVATE ${GLPK_LIBRARIES})
-  if(ENABLE_STATIC_LIBRARY)
+  if(ENABLE_STATIC_BUILD)
     target_link_libraries(cvc5-static PUBLIC ${GLPK_LIBRARIES})
   endif()
 endif()
@@ -1422,7 +1422,7 @@ if(USE_POLY)
   add_dependencies(cvc5-obj Polyxx_SHARED)
   target_include_directories(cvc5-obj PRIVATE ${Poly_INCLUDE_DIR})
   target_link_libraries(cvc5-shared PRIVATE Polyxx_SHARED)
-  if(ENABLE_STATIC_LIBRARY)
+  if(ENABLE_STATIC_BUILD)
     target_link_libraries(cvc5-static PUBLIC Polyxx_STATIC)
   endif()
 endif()
@@ -1430,7 +1430,7 @@ if(USE_COCOA)
   add_dependencies(cvc5-obj CoCoA)
   target_include_directories(cvc5-obj PRIVATE ${CoCoA_INCLUDE_DIR})
   target_link_libraries(cvc5-shared PRIVATE CoCoA)
-  if(ENABLE_STATIC_LIBRARY)
+  if(ENABLE_STATIC_BUILD)
     target_link_libraries(cvc5-static PUBLIC CoCoA)
   endif()
 endif()
@@ -1438,7 +1438,7 @@ endif()
 add_dependencies(cvc5-obj SymFPU)
 target_include_directories(cvc5-obj PRIVATE ${SymFPU_INCLUDE_DIR})
 target_link_libraries(cvc5-shared PRIVATE SymFPU)
-if(ENABLE_STATIC_LIBRARY)
+if(ENABLE_STATIC_BUILD)
   target_link_libraries(cvc5-static PUBLIC SymFPU)
 endif()
 

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index a16baeb73e8b64b3fdd3cd22d639343920d1e3d6..cb83413f9a43831cfe71d2b71bbe675a7441bf75 100644 (file)
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -76,7 +76,7 @@ endif()
 # use the static system libraries.
 #   https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_START_STATIC.html
 #   https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_END_STATIC.html
-if(ENABLE_STATIC_BINARY)
+if(ENABLE_STATIC_BUILD)
   if(NOT CMAKE_SYSTEM_NAME STREQUAL "Darwin")
     set_target_properties(cvc5-bin PROPERTIES LINK_FLAGS -static)
     set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_START_STATIC ON)

diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 92648638cea87b976a9507746be721cc1a0f274e..d012851d7c84984dc9dfa45337b6035e54e0a8f4 100644 (file)
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -124,7 +124,7 @@ install(TARGETS cvc5parser-shared
   EXPORT cvc5-targets
   DESTINATION ${CMAKE_INSTALL_LIBDIR})
 
-if(ENABLE_STATIC_LIBRARY)
+if(ENABLE_STATIC_BUILD)
   add_library(cvc5parser-static STATIC $<TARGET_OBJECTS:cvc5parser-objs>)
   set_target_properties(cvc5parser-static PROPERTIES OUTPUT_NAME cvc5parser)
   target_link_libraries(cvc5parser-static PRIVATE cvc5-static)