From 27413a45e28001f6155d529a59d679556cdc011e Mon Sep 17 00:00:00 2001 From: makaimann Date: Wed, 12 Aug 2020 12:03:45 -0700 Subject: [PATCH] Add option to only build library (#4801) This PR would add an option to only build the CVC4 library and not the parser or executable. This can be used for projects that only intend to use CVC4 through the API. It seems to be working now, but it's not necessarily the cleanest solution. In particular, if you'd like the polarity to be different I'm happy to change that. Polarity meaning something like "${WITH_BINARY}" STREQUAL "YES" instead of NOT "${LIB_ONLY} STREQUAL "YES" which is admittedly a little strange. --- CMakeLists.txt | 5 +++++ configure.sh | 10 ++++++++++ src/CMakeLists.txt | 8 ++++++-- test/CMakeLists.txt | 4 +++- 4 files changed, 24 insertions(+), 3 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 2d658ee31..5b1d1e292 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -174,6 +174,9 @@ 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") + #-----------------------------------------------------------------------------# # Internal cmake variables @@ -709,6 +712,8 @@ print_config("GLPK :" USE_GLPK) print_config("Kissat :" USE_KISSAT) print_config("LFSC :" USE_LFSC) print_config("LibPoly :" USE_POLY) +message("") +print_config("BUILD_LIB_ONLY :" BUILD_LIB_ONLY) if(CVC4_USE_CLN_IMP) message("MP library : cln") diff --git a/configure.sh b/configure.sh index 3bce5a548..48d1b82b2 100755 --- a/configure.sh +++ b/configure.sh @@ -80,6 +80,10 @@ Optional Path to Optional Packages: --poly-dir=PATH path to top level of LibPoly source tree --symfpu-dir=PATH path to top level of SymFPU source tree +Build limitations: + --lib-only only build the library, but not the executable or + the parser (default: off) + EOF exit 0 } @@ -161,6 +165,8 @@ lfsc_dir=default poly_dir=default symfpu_dir=default +lib_only=default + #--------------------------------------------------------------------------# while [ $# -gt 0 ] @@ -334,6 +340,8 @@ do --symfpu-dir) die "missing argument to $1 (try -h)" ;; --symfpu-dir=*) symfpu_dir=${1##*=} ;; + --lib-only) lib_only=ON ;; + -*) die "invalid option '$1' (try -h)";; *) case $1 in @@ -455,6 +463,8 @@ cmake_opts="" && cmake_opts="$cmake_opts -DPOLY_DIR=$poly_dir" [ "$symfpu_dir" != default ] \ && cmake_opts="$cmake_opts -DSYMFPU_DIR=$symfpu_dir" +[ "$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 2a5639e9e..67692f5c0 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -867,7 +867,9 @@ set(KINDS_FILES add_subdirectory(base) add_subdirectory(expr) add_subdirectory(options) -add_subdirectory(parser) +if (NOT BUILD_LIB_ONLY) + add_subdirectory(parser) +endif() add_subdirectory(theory) add_subdirectory(util) @@ -959,7 +961,9 @@ target_link_libraries(cvc4 ${RT_LIBRARIES}) # target_link_libraries(...) with object libraries for cmake versions <= 3.12. # Thus, we can only visit main as soon as all dependencies for cvc4 are set up. -add_subdirectory(main) +if (NOT BUILD_LIB_ONLY) + add_subdirectory(main) +endif() #-----------------------------------------------------------------------------# # Note: diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 52a999c1b..cc05aff43 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -21,7 +21,9 @@ add_custom_target(check #-----------------------------------------------------------------------------# # Add subdirectories -add_subdirectory(regress) +if (NOT BUILD_LIB_ONLY) + add_subdirectory(regress) +endif() add_subdirectory(system EXCLUDE_FROM_ALL) if(ENABLE_UNIT_TESTING) -- 2.30.2