Add documentation and build instructions for recompilation (LGPL). (#4844)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 93ea5cbebc7aec2b3de677b071c0f223fe79a132..2d658ee3193af558ca8abc7383eb703364889a86 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -548,7 +548,11 @@ endif()
 # Generate CVC4's cvc4autoconfig.h header
 
 include(ConfigureCVC4)
+if(NOT ENABLE_SHARED)
+  set(CVC4_STATIC_BUILD ON)
+endif()
 configure_file(cvc4autoconfig.h.in cvc4autoconfig.h)
+unset(CVC4_STATIC_BUILD)
 include_directories(${CMAKE_CURRENT_BINARY_DIR})
 
 #-----------------------------------------------------------------------------#

diff --git a/INSTALL.md b/INSTALL.md
index a5b0481312e842a7d854558fd5fa8b89e7922513..7143dfc0ed3db12bfe4e12395591a9aa5aa6a23c 100644 (file)
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -317,3 +317,36 @@ are configured to **run** in parallel with the maximum number of threads
 available on the system. Override with `ARGS=-jN`.
 
 Use `-jN` for parallel **building** with `N` threads.
+
+
+## Recompiling a specific CVC4 version with different LGPL library versions
+
+To recompile a specific static binary of CVC4 with different versions of the
+linked LGPL libraries perform the following steps:
+
+1. Make sure that you have installed the desired LGPL library versions.
+   You can check the versions found by CVC4's build system during the configure
+   phase.
+
+2. Determine the commit sha and configuration of the CVC4 binary
+```
+cvc4 --show-config
+```
+3. Download the specific source code version:
+```
+wget https://github.com/CVC4/CVC4/archive/<commit-sha>.tar.gz
+```
+4. Extract the source code
+```
+tar xf <commit-sha>.tar.gz
+```
+5. Change into source code directory
+```
+cd CVC4-<commit-sha>
+```
+6. Configure CVC4 with options listed by `cvc4 --show-config`
+```
+./configure.sh --static <options>
+```
+
+7. Follow remaining steps from [build instructions](#building-cvc4)

diff --git a/cvc4autoconfig.h.in b/cvc4autoconfig.h.in
index 603670a3a47cd7e6e51aee73d44a0f3f73934a71..48d826697b01935a5738c6023e71bbb9291d5c80 100644 (file)
--- a/cvc4autoconfig.h.in
+++ b/cvc4autoconfig.h.in
@@ -64,4 +64,6 @@
 /* Define to 1 if `strerror_r' returns (char *). */
 #cmakedefine01 STRERROR_R_CHAR_P
 
+#cmakedefine01 CVC4_STATIC_BUILD
+
 #endif /* __CVC4__CVC4AUTOCONFIG_H */

diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index ef20b47cb6d159957042ff5c4a961b50f46e3a87..9da81325363560a75182ce20f92c12d87b764038 100644 (file)
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -88,6 +88,15 @@ bool Configuration::isCompetitionBuild() {
   return IS_COMPETITION_BUILD;
 }
 
+bool Configuration::isStaticBuild()
+{
+#if defined(CVC4_STATIC_BUILD)
+  return true;
+#else
+  return false;
+#endif
+}
+
 string Configuration::getPackageName() {
   return CVC4_PACKAGE_NAME;
 }
@@ -201,6 +210,13 @@ std::string Configuration::copyright() {
          << "  See https://github.com/SRI-CSL/libpoly for copyright and\n"
          << "  licensing information.\n\n";
     }
+    if (Configuration::isStaticBuild())
+    {
+      ss << "CVC4 is statically linked against these libraries. To recompile\n"
+            "this version of CVC4 with different versions of these libraries\n"
+            "follow the instructions on "
+            "https://github.com/CVC4/CVC4/blob/master/INSTALL.md\n\n";
+    }
   }
 
   if (Configuration::isBuiltWithCln()

diff --git a/src/base/configuration.h b/src/base/configuration.h
index d148adcbbb6221346a06ed32e978130503bb1384..9d558f502b98791f9dc0b18965ebdb34d721d0db 100644 (file)
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -69,6 +69,8 @@ public:
 
   static bool isCompetitionBuild();
 
+  static bool isStaticBuild();
+
   static std::string getPackageName();
 
   static std::string getVersionString();