From 99640a4dc014177ed3b205b7186254933e7c5566 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 4 Aug 2020 14:03:36 -0700
Subject: [PATCH] Add documentation and build instructions for recompilation
 (LGPL). (#4844)

---
 CMakeLists.txt             |  4 ++++
 INSTALL.md                 | 33 +++++++++++++++++++++++++++++++++
 cvc4autoconfig.h.in        |  2 ++
 src/base/configuration.cpp | 16 ++++++++++++++++
 src/base/configuration.h   |  2 ++
 5 files changed, 57 insertions(+)

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();
-- 
2.30.2