From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 4 Aug 2020 21:03:36 +0000 (-0700)
Subject: Add documentation and build instructions for recompilation (LGPL). (#4844)
X-Git-Tag: cvc5-1.0.0~3042
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=99640a4dc014177ed3b205b7186254933e7c5566;p=cvc5.git

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

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 93ea5cbeb..2d658ee31 100644
--- 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 a5b048131..7143dfc0e 100644
--- 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 603670a3a..48d826697 100644
--- 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 ef20b47cb..9da813253 100644
--- 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 d148adcbb..9d558f502 100644
--- 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();