diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-09-07 14:14:56 -0700 |
---|---|---|
committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-22 16:30:59 -0700 |
commit | e0dc035348aa4bd22d0964539803775d0cbb21ac (patch) | |
tree | 0f126679ce35bff8a52e51f230c626b6da5e97e4 /configure.sh | |
parent | bb137cf7d56cbd850c29e0b496e2e5ca4a856a76 (diff) |
cmake: configure.sh wrapper: done (except: configurable build dir)
Diffstat (limited to 'configure.sh')
-rwxr-xr-x | configure.sh | 324 |
1 files changed, 213 insertions, 111 deletions
diff --git a/configure.sh b/configure.sh index 82ec89646..8ab1927cf 100755 --- a/configure.sh +++ b/configure.sh @@ -13,34 +13,28 @@ Build types: General options; - -h, --help display this help and exit - - --gpl permit GPL dependences, if available - --best turn on dependences known to give best performance + -h, --help display this help and exit + --gpl permit GPL dependences, if available + --best turn on dependences known to give best performance Features: - The following flags enable optional features (disable with --no-<option name>). - - --static build static libraries and binaries [default=no] - - --proofs support for proof generation - --optimized optimize the build - --debug-symbols include debug symbols - --valgrind Valgrind instrumentation - --debug-context-memory-manager - use the debug context memory manager - --statistics do not include statistics - --replay turn off the replay feature - --assertions turn off assertions - --tracing remove all tracing code - --dumping remove all dumping code - --muzzle complete silence (no non-result output) - --coverage support for gcov coverage testing - --profiling support for gprof profiling - --unit-testing support for unit testing - --thread-support support for multithreaded-capable library + --static build static libraries and binaries [default=no] + --proofs support for proof generation + --optimized optimize the build + --debug-symbols include debug symbols + --valgrind Valgrind instrumentation + --debug-context-mm use the debug context memory manager + --statistics do not include statistics + --replay turn off the replay feature + --assertions turn off assertions + --tracing remove all tracing code + --dumping remove all dumping code + --muzzle complete silence (no non-result output) + --coverage support for gcov coverage testing + --profiling support for gprof profiling + --unit-testing support for unit testing The following options configure parameterized features. @@ -48,29 +42,28 @@ The following options configure parameterized features. specify language bindings to build Optional Packages: - - --cln use CLN instead of GMP - --gmp use GMP instead of CLN - --glpk use GLPK simplex solver - --glpk-dir=PATH path to top level of glpk installation - --abc use the ABC AIG library - --abc-dir=PATH path to top level of abc source tree - --cadical use the CaDiCaL SAT solver - --cadical-dir=PATH path to top level of CaDiCaL source tree - --cryptominisat use the CRYPTOMINISAT sat solver - --cryptominisat-dir=PATH - path to top level of cryptominisat source tree - --lfsc use the LFSC proof checker - --lfsc-dir=PATH path to top level of lfsc source tree - --symfpu use symfpu for floating point solver - --symfpu-dir=PATH path to top level of symfpu source tree - --cxxtest-dir=DIR path to CxxTest installation - --antlr-dir=PATH path to ANTLR C headers and libraries - --swig=BINARY path to swig binary - --boost=DIR prefix of Boost [guess] - --portfolio build the multithreaded portfolio version of CVC4 - (pcvc4) - --readline support the readline library +The following flags enable optional packages (disable with --no-<option name>). + --cln use CLN instead of GMP + --gmp use GMP instead of CLN + --glpk use GLPK simplex solver + --abc use the ABC AIG library + --cadical use the CaDiCaL SAT solver + --cryptominisat use the CRYPTOMINISAT sat solver + --lfsc use the LFSC proof checker + --symfpu use symfpu for floating point solver + --portfolio build the multithreaded portfolio version of CVC4 + (pcvc4) + --readline support the readline library + +Optional Path to Optional Packages: + --abc-dir=PATH path to top level of abc source tree + --antlr-dir=PATH path to ANTLR C headers and libraries + --cadical-dir=PATH path to top level of CaDiCaL source tree + --cryptominisat-dir=PATH path to top level of cryptominisat source tree + --cxxtest-dir=DIR path to CxxTest installation + --glpk-dir=PATH path to top level of glpk installation + --lfsc-dir=PATH path to top level of lfsc source tree + --symfpu-dir=PATH path to top level of symfpu source tree Report bugs to <cvc4-bugs@cs.stanford.edu>. EOF @@ -170,45 +163,44 @@ BUILDDIR=build #--------------------------------------------------------------------------# -buildtype=production - -abc=no -asan=no -assertions=no -best=no -bsd=no -cadical=no -cln=no -coverage=no -cryptominisat=no -debug_symbols=no -debug_context_mm=no -dumping=no -gpl=no -glpk=no -glpk_dir=no -language_bindings=no -lfsc=no -muzzle=no -optimized=no -portfolio=no -proofs=no -replay=no -static=no -statistics=no -symfpu=no -tracing=no -unit_testing=no -valgrind=no -profiling=no -readline=no -thread_support=no +buildtype=default + +abc=default +asan=default +assertions=default +best=default +cadical=default +cln=default +coverage=default +cryptominisat=default +debug_symbols=default +debug_context_mm=default +dumping=default +gpl=default +glpk=default +lfsc=default +muzzle=default +optimized=default +portfolio=default +proofs=default +replay=default +static=default +statistics=default +symfpu=default +tracing=default +unit_testing=default +valgrind=default +profiling=default +readline=default + +language_bindings=default abc_dir=default antlr_dir=default cadical_dir=default cryptominisat_dir=default cxxtest_dir=default +glpk_dir=default lfsc_dir=default symfpu_dir=default @@ -217,35 +209,89 @@ symfpu_dir=default while [ $# -gt 0 ] do case $1 in - --abc) abc=yes;; - --asan) asan=yes;; - --assertions) assertions=yes;; - --best) best=yes;; - --cadical) cadical=yes;; - --cln) cln=yes;; - --coverage) coverage=yes;; - --cryptominisat) cryptominisat=yes;; - --debug-symbols) debug_symbols;; - --debug-context-memory-manager) debug_context_mm=yes;; - --dumping) dumping=yes;; - --gpl) gpl=yes;; - --glpk) glpk=yes;; + -h|--help) usage;; - --lfsc) lfsc=yes;; - --muzzle) muzzle=yes;; - --optimized) optimized=yes;; - --portfolio) portfolio=yes;; - --proofs) proofs=yes;; - --replay) replay=yes;; - --static) static=yes;; - --statistics) statistics=yes;; - --symfpu) symfpu=yes;; - --tracing) tracing=yes;; - --unit-testing) unit_testing=yes;; - --valgrind) valgrind=yes;; - --profiling) profiling=yes;; - --readline) readline=yes;; - --thread-support) thread_support=yes;; + + --abc) abc=ON;; + --no-abc) abc=OFF;; + + --asan) asan=ON;; + --no-asan) asan=OFF;; + + --assertions) assertions=ON;; + --no-assertions) assertions=OFF;; + + --best) best=ON;; + --no-best) best=OFF;; + + --cadical) cadical=ON;; + --no-cadical) cadical=OFF;; + + --cln) cln=ON;; + --no-cln) cln=OFF;; + + --coverage) coverage=ON;; + --no-coverage) coverage=OFF;; + + --cryptominisat) cryptominisat=ON;; + --no-cryptominisat) cryptominisat=OFF;; + + --debug-symbols) debug_symbols=ON;; + --no-debug-symbols) debug_symbols=OFF;; + + --debug-context-memory-manager) debug_context_mm=ON;; + --no-debug-context-memory-manager) debug_context_mm=OFF;; + + --dumping) dumping=ON;; + --no-dumping) dumping=OFF;; + + --gpl) gpl=ON;; + --no-gpl) gpl=OFF;; + + --glpk) glpk=ON;; + --no-glpk) glpk=OFF;; + + --lfsc) lfsc=ON;; + --no-lfsc) lfsc=OFF;; + + --muzzle) muzzle=ON;; + --no-muzzle) muzzle=OFF;; + + --optimized) optimized=ON;; + --no-optimized) optimized=OFF;; + + --portfolio) portfolio=ON;; + --no-portfolio) portfolio=OFF;; + + --proofs) proofs=ON;; + --no-proofs) proofs=OFF;; + + --replay) replay=ON;; + --no-replay) replay=OFF;; + + --static) static=ON;; + --no-static) static=OFF;; + + --statistics) statistics=ON;; + --no-statistics) statistics=OFF;; + + --symfpu) symfpu=ON;; + --no-symfpu) symfpu=OFF;; + + --tracing) tracing=ON;; + --no-tracing) tracing=OFF;; + + --unit-testing) unit_testing=ON;; + --no-unit-testing) unit_testing=OFF;; + + --valgrind) valgrind=ON;; + --no-valgrind) valgrind=OFF;; + + --profiling) profiling=ON;; + --no-profiling) profiling=OFF;; + + --readline) readline=ON;; + --no-readline) readline=OFF;; --language-bindings) shift @@ -325,10 +371,66 @@ do -*) die "invalid option '$1' (try '-h')";; - *) [[ "production debug testing competition" =~ (^|[[:space:]])"$1"($|[[:space:]]) ]] \ - || die "invalid build type (try '-h')" - buildtype=$1 + *) case $1 in + production) buildtype=Production;; + debug) buildtype=Debug;; + testing) buildtype=Testing;; + competition) buildtype=Competition;; + *) die "invalid build type (try '-h')";; + esac ;; esac shift done + +#--------------------------------------------------------------------------# + +cmake_opts="" + +[ $buildtype != default ] && cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype" + +[ $asan != default ] && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan" +[ $assertions != default ] && cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions" +[ $best != default ] && cmake_opts="$cmake_opts -DENABLE_BEST=$best" +[ $coverage != default ] && cmake_opts="$cmake_opts -DENABLE_COVERAGE=$coverage" +[ $debug_symbols != default ] && cmake_opts="$cmake_opts -DENABLE_DEBUG_SYMBOLS=$debug_symbols" +[ $debug_context_mm != default ] && cmake_opts="$cmake_opts -DENABLE_DEBUG_CONTEXT_MM=$debug_context_mm" +[ $dumping != default ] && cmake_opts="$cmake_opts -DENABLE_DUMPING=$dumping" +[ $gpl != default ] && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl" +[ $muzzle != default ] && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle" +[ $optimized != default ] && cmake_opts="$cmake_opts -DENABLE_OPTIMIZED=$optimized" +[ $portfolio != default ] && cmake_opts="$cmake_opts -DENABLE_PORTFOLIO=$portfolio" +[ $proofs != default ] && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs" +[ $replay != default ] && cmake_opts="$cmake_opts -DENABLE_REPLAY=$replay" +[ $static != default ] && cmake_opts="$cmake_opts -DENABLE_STATIC=$static" +[ $statistics != default ] && cmake_opts="$cmake_opts -DENABLE_STATISTICS=$statistics" +[ $tracing != default ] && cmake_opts="$cmake_opts -DENABLE_TRACING=$tracing" +[ $unit_testing != default ] && cmake_opts="$cmake_opts -DENABLE_UNIT_TESTING=$unit_testing" +[ $valgrind != default ] && cmake_opts="$cmake_opts -DENABLE_VALGRIND=$valgrind" +[ $profiling != default ] && cmake_opts="$cmake_opts -DENABLE_PROFILING=$profiling" +[ $readline != default ] && cmake_opts="$cmake_opts -DENABLE_READLINE=$readline" + +[ $abc != default ] && cmake_opts="$cmake_opts -DUSE_ABC=$abc" +[ $cadical != default ] && cmake_opts="$cmake_opts -DUSE_CADICAL=$cadical" +[ $cln != default ] && cmake_opts="$cmake_opts -DUSE_CLN=$cln" +[ $cryptominisat != default ] && cmake_opts="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat" +[ $glpk != default ] && cmake_opts="$cmake_opts -DUSE_GLPK=$glpk" +[ $lfsc != default ] && cmake_opts="$cmake_opts -DUSE_LFSC=$lfsc" +[ $symfpu != default ] && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu" + +[ $language_bindings != default ] && cmake_opts="$cmake_opts -DENABLE_LANGUAGE_BINDINGS=$language_bindings" + +[ $abc_dir != default ] && cmake_opts="$cmake_opts -DENABLE_ABC_DIR=$abc_dir" +[ $antlr_dir != default ] && cmake_opts="$cmake_opts -DENABLE_ANTLR_DIR=$antlr_dir" +[ $cadical_dir != default ] && cmake_opts="$cmake_opts -DENABLE_CADICAL_DIR=$cadical_dir" +[ $cryptominisat_dir != default ] && cmake_opts="$cmake_opts -DENABLE_CRYPTOMINISAT_DIR=$cryptominisat_dir" +[ $cxxtest_dir != default ] && cmake_opts="$cmake_opts -DENABLE_CXXTEST_DIR=$cxxtest_dir" +[ $glpk_dir != default ] && cmake_opts="$cmake_opts -DENABLE_GLPL_DIR=$glpk_dir" +[ $lfsc_dir != default ] && cmake_opts="$cmake_opts -DENABLE_LFSC_DIR=$lfsc_dir" +[ $symfpu_dir != default ] && cmake_opts="$cmake_opts -DENABLE_SYMFPU_DIR=$symfpu_dir" + +mkdir -p $BUILDDIR +cd $BUILDDIR + +[ -e CMakeCache.txt ] && rm CMakeCache.txt +cmake .. $cmake_opts |