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.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index e2e24ecf13207d00d14c0b8ae0c3b7f559a231c7..054d4938ccb7f0e1b54699e9b2149d272657ffcf 100644 (file)
--- 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 0db8659cada7264c7b868a009c741791b05dc2bb..07c1cc4aed6ea888cbeeb8d2e28a03954cfa7e33 100755 (executable)
--- 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 c7192dcf7592cc29badb457252af72696ef4b516..13ab74d4b379d0dc4baf09cb7d291a0ffd5c12d5 100644 (file)
--- 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 ac184899473ceb7837168b951724110d46e90d14..d3ff709ca30f63025436e3be137bad8415899ea5 100644 (file)
--- 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)