Enable static builds in CI (#7281)

This PR modifies our CI builds to have two static production builds. These binaries will be used as release artifacts later.

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 6c7c4ed236b4b617548bfbd9d882bc3319ace569..6cea1122f14804ce1e98c4b45fc11481c102e422 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
+            config: production --auto-download --all-bindings --editline --docs --static-binary
             cache-key: production
             python-bindings: true
             build-documentation: true
@@ -18,7 +18,7 @@ jobs:
 
           - name: macos:production
             os: macos-11
-            config: production --auto-download --all-bindings --editline
+            config: production --auto-download --all-bindings --editline --static-binary
             cache-key: production
             python-bindings: true
             check-examples: true
@@ -64,10 +64,12 @@ jobs:
         sudo apt-get install -y \
           build-essential \
           ccache \
+          libbsd-dev \
           libcln-dev \
+          libedit-dev \
           libgmp-dev \
           libgtest-dev \
-          libedit-dev \
+          libtinfo-dev \
           flex \
           libfl-dev \
           flexc++

diff --git a/INSTALL.rst b/INSTALL.rst
index 99626a554ec7d937d358fbac68d858919ee8b499..7df21cb4cf18cec71bb8875e5d0cc5dcb134acd8 100644 (file)
--- a/INSTALL.rst
+++ b/INSTALL.rst
@@ -31,8 +31,11 @@ Compilation on macOS
 On macOS, we recommend using `Homebrew <https://brew.sh/>`_ to install the
 dependencies.  We also have a Homebrew Tap available at
 https://github.com/CVC4/homebrew-cvc4 .
-To build a static binary for macOS, use:
-``./configure.sh --static --no-static-binary``.
+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
+that uses static versions of all our dependencies, but is still a dynamically
+linked binary.
 
 
 Cross-compiling for Windows
@@ -42,7 +45,7 @@ Cross-compiling cvc5 with Mingw-w64 can be done as follows:
 
 .. code:: bash
 
-  ./configure.sh --win64 --static <configure options...>
+  ./configure.sh --win64 --static-binary <configure options...>
 
   cd <build_dir>   # default is ./build
   make             # use -jN for parallel build with N threads
@@ -428,6 +431,6 @@ linked LGPL libraries perform the following steps:
 
 .. code::
   
-  ./configure.sh --static <options>
+  ./configure.sh --static-binary <options>
 
 7. Follow remaining steps from `build instructions <#building-cvc5>`_

diff --git a/cmake/deps-helper.cmake b/cmake/deps-helper.cmake
index f2a43c0286387000539ed12935d7fa6a8f5f055b..9a92928b6092d00b91fe7bd27848c9ff46c7b9e4 100644 (file)
--- a/cmake/deps-helper.cmake
+++ b/cmake/deps-helper.cmake
@@ -40,7 +40,6 @@ if(CMAKE_VERSION VERSION_GREATER_EQUAL "3.14")
 endif()
 
 macro(force_static_library)
-    message(STATUS "before: ${CMAKE_FIND_LIBRARY_SUFFIXES}")
     if (WIN32)
         set(CMAKE_FIND_LIBRARY_SUFFIXES .lib .a)
     else()
@@ -50,9 +49,9 @@ endmacro(force_static_library)
 
 macro(reset_force_static_library)
     if (WIN32)
-        set(CMAKE_FIND_LIBRARY_SUFFIXES .dll)
+        set(CMAKE_FIND_LIBRARY_SUFFIXES .dll .lib)
     else()
-        set(CMAKE_FIND_LIBRARY_SUFFIXES .so .dylib)
+        set(CMAKE_FIND_LIBRARY_SUFFIXES .so .dylib .a)
     endif()
 endmacro(reset_force_static_library)
 

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 4d528312e6a9c55fc3d63301e7937fe9d70008ce..1aedcb265c36e07311b60b24c9a6623edfd172d8 100644 (file)
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -78,9 +78,11 @@ endif()
 #   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)
-  set_target_properties(cvc5-bin PROPERTIES LINK_FLAGS -static)
-  set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_START_STATIC ON)
-  set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_END_STATIC ON)
+  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)
+    set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_END_STATIC ON)
+  endif()
 endif()
 
 if(USE_EDITLINE)