From a42b56e46f579b57eb0a3f49d1195881670375e7 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <nafur42@gmail.com>
Date: Tue, 28 Sep 2021 20:10:45 -0700
Subject: [PATCH] remove stuff (#7258)

This PR removes the BUILD_LIB_ONLY cmake option, and the associated --lib-only configure script option.
If you only want the library, just run make cvc5 instead of make.
---
 CMakeLists.txt      | 5 -----
 configure.sh        | 5 -----
 src/CMakeLists.txt  | 8 ++------
 test/CMakeLists.txt | 4 +---
 4 files changed, 3 insertions(+), 19 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index e2e24ecf1..054d4938c 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -146,9 +146,6 @@ set(PROGRAM_PREFIX    "" CACHE STRING "Program prefix on make install")
 option(BUILD_BINDINGS_PYTHON "Build Python bindings based on new C++ API ")
 option(BUILD_BINDINGS_JAVA "Build Java bindings based on new C++ API ")
 
-# Build limitations
-option(BUILD_LIB_ONLY         "Only build the library")
-
 # Api documentation
 cvc5_option(BUILD_DOCS "Build Api documentation")
 
@@ -678,8 +675,6 @@ print_config("GLPK                      " ${USE_GLPK})
 print_config("Kissat                    " ${USE_KISSAT} FOUND_SYSTEM ${Kissat_FOUND_SYSTEM})
 print_config("LibPoly                   " ${USE_POLY} FOUND_SYSTEM ${Poly_FOUND_SYSTEM})
 print_config("CoCoALib                  " ${USE_COCOA} FOUND_SYSTEM ${CoCoA_FOUND_SYSTEM})
-message("")
-print_config("Build libcvc5 only        " ${BUILD_LIB_ONLY})
 
 if(CVC5_USE_CLN_IMP)
   print_config("MP library                " "cln" FOUND_SYSTEM ${CLN_FOUND_SYSTEM})
diff --git a/configure.sh b/configure.sh
index 0db8659ca..07c1cc4ae 100755
--- a/configure.sh
+++ b/configure.sh
@@ -147,8 +147,6 @@ ipo=default
 abc_dir=default
 glpk_dir=default
 
-lib_only=default
-
 #--------------------------------------------------------------------------#
 
 cmake_opts=""
@@ -300,7 +298,6 @@ do
     --dep-path) die "missing argument to $1 (try -h)" ;;
     --dep-path=*) dep_path="${dep_path};${1##*=}" ;;
 
-    --lib-only) lib_only=ON ;;
     -D*) cmake_opts="${cmake_opts} $1" ;;
 
     -*) die "invalid option '$1' (try -h)";;
@@ -403,8 +400,6 @@ fi
   && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir"
 [ "$dep_path" != default ] \
   && cmake_opts="$cmake_opts -DCMAKE_PREFIX_PATH=$dep_path"
-[ "$lib_only" != default ] \
-    && cmake_opts="$cmake_opts -DBUILD_LIB_ONLY=$lib_only"
 [ "$install_prefix" != default ] \
   && cmake_opts="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix"
 [ -n "$program_prefix" ] \
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c7192dcf7..13ab74d4b 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1284,9 +1284,7 @@ set(KINDS_FILES
 add_subdirectory(base)
 add_subdirectory(context)
 add_subdirectory(expr)
-if (NOT BUILD_LIB_ONLY)
-  add_subdirectory(parser)
-endif()
+add_subdirectory(parser)
 add_subdirectory(theory)
 add_subdirectory(util)
 
@@ -1359,9 +1357,7 @@ target_link_libraries(cvc5 PRIVATE GMP)
 # target_link_libraries(...) with object libraries for cmake versions <= 3.12.
 # Thus, we can only visit main as soon as all dependencies for cvc5 are set up.
 
-if (NOT BUILD_LIB_ONLY)
-  add_subdirectory(main)
-endif()
+add_subdirectory(main)
 
 #-----------------------------------------------------------------------------#
 # Install public API headers
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index ac1848994..d3ff709ca 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -35,9 +35,7 @@ add_custom_target(check
 #-----------------------------------------------------------------------------#
 # Add subdirectories
 
-if (NOT BUILD_LIB_ONLY)
-  add_subdirectory(regress)
-endif()
+add_subdirectory(regress)
 add_subdirectory(api EXCLUDE_FROM_ALL)
 
 if(ENABLE_UNIT_TESTING)
-- 
2.30.2