configure.sh

   1 #!/bin/sh
   2 #--------------------------------------------------------------------------#
   3
   4 usage () {
   5 cat <<EOF
   6 Usage: $0 [<build type>] [<option> ...]
   7
   8 Build types:
   9   production
  10   debug
  11   testing
  12   competition
  13
  14
  15 General options;
  16   -h, --help               display this help and exit
  17   --prefix=STR             install directory
  18   --build-prefix=STR       prefix build directory with given prefix
  19   --name=STR               use custom build directory name
  20   --best                   turn on dependences known to give best performance
  21   --gpl                    permit GPL dependences, if available
  22   --win64                  cross-compile for Windows 64 bit
  23
  24
  25 Features:
  26 The following flags enable optional features (disable with --no-<option name>).
  27   --static                 build static libraries and binaries [default=no]
  28   --proofs                 support for proof generation
  29   --optimized              optimize the build
  30   --debug-symbols          include debug symbols
  31   --valgrind               Valgrind instrumentation
  32   --debug-context-mm       use the debug context memory manager
  33   --statistics             do not include statistics
  34   --replay                 turn off the replay feature
  35   --assertions             turn off assertions
  36   --tracing                remove all tracing code
  37   --dumping                remove all dumping code
  38   --muzzle                 complete silence (no non-result output)
  39   --coverage               support for gcov coverage testing
  40   --profiling              support for gprof profiling
  41   --unit-testing           support for unit testing
  42   --python2                prefer using Python 2 (for Python bindings)
  43
  44 The following options configure parameterized features.
  45
  46   --language-bindings[=java,python,all]
  47                           specify language bindings to build
  48
  49 Optional Packages:
  50 The following flags enable optional packages (disable with --no-<option name>).
  51   --cln                    use CLN instead of GMP
  52   --gmp                    use GMP instead of CLN
  53   --glpk                   use GLPK simplex solver
  54   --abc                    use the ABC AIG library
  55   --cadical                use the CaDiCaL SAT solver
  56   --cryptominisat          use the CRYPTOMINISAT sat solver
  57   --lfsc                   use the LFSC proof checker
  58   --symfpu                 use symfpu for floating point solver
  59   --portfolio              build the multithreaded portfolio version of CVC4
  60                            (pcvc4)
  61   --readline               support the readline library
  62
  63 Optional Path to Optional Packages:
  64   --abc-dir=PATH           path to top level of abc source tree
  65   --antlr-dir=PATH         path to ANTLR C headers and libraries
  66   --cadical-dir=PATH       path to top level of CaDiCaL source tree
  67   --cryptominisat-dir=PATH path to top level of cryptominisat source tree
  68   --cxxtest-dir=DIR        path to CxxTest installation
  69   --glpk-dir=PATH          path to top level of glpk installation
  70   --gmp-dir=PATH           path to top level of GMP installation
  71   --lfsc-dir=PATH          path to top level of lfsc source tree
  72   --symfpu-dir=PATH        path to top level of symfpu source tree
  73
  74 Report bugs to <cvc4-bugs@cs.stanford.edu>.
  75 EOF
  76   exit 0
  77 }
  78
  79 #--------------------------------------------------------------------------#
  80
  81 die () {
  82   echo "*** configure.sh: $*" 1>&2
  83   exit 1
  84 }
  85
  86 msg () {
  87   echo "[configure.sh] $*"
  88 }
  89
  90 #--------------------------------------------------------------------------#
  91
  92 [ ! -e src/theory ] && die "$0 not called from CVC4 base directory"
  93
  94 #--------------------------------------------------------------------------#
  95
  96 build_dir=production
  97 install_prefix=default
  98 build_prefix=""
  99 build_name=""
 100
 101 #--------------------------------------------------------------------------#
 102
 103 buildtype=default
 104
 105 abc=default
 106 asan=default
 107 assertions=default
 108 best=default
 109 cadical=default
 110 cln=default
 111 coverage=default
 112 cryptominisat=default
 113 debug_symbols=default
 114 debug_context_mm=default
 115 dumping=default
 116 gpl=default
 117 win64=default
 118 glpk=default
 119 lfsc=default
 120 muzzle=default
 121 optimized=default
 122 portfolio=default
 123 proofs=default
 124 replay=default
 125 shared=default
 126 statistics=default
 127 symfpu=default
 128 tracing=default
 129 unit_testing=default
 130 python2=default
 131 valgrind=default
 132 profiling=default
 133 readline=default
 134
 135 language_bindings_java=default
 136 language_bindings_python=default
 137
 138 abc_dir=default
 139 antlr_dir=default
 140 cadical_dir=default
 141 cryptominisat_dir=default
 142 glpk_dir=default
 143 gmp_dir=default
 144 lfsc_dir=default
 145 symfpu_dir=default
 146
 147 #--------------------------------------------------------------------------#
 148
 149 while [ $# -gt 0 ]
 150 do
 151   case $1 in
 152
 153     -h|--help) usage;;
 154
 155     --abc) abc=ON;;
 156     --no-abc) abc=OFF;;
 157
 158     --asan) asan=ON;;
 159     --no-asan) asan=OFF;;
 160
 161     --assertions) assertions=ON;;
 162     --no-assertions) assertions=OFF;;
 163
 164     --best) best=ON;;
 165     --no-best) best=OFF;;
 166
 167     --prefix) die "missing argument to $1 (try -h)" ;;
 168     --prefix=*)
 169         install_prefix=${1##*=}
 170         # Check if install_prefix is an absolute path and if not, make it
 171         # absolute.
 172         case $install_prefix in
 173           /*) ;;                                      # absolute path
 174           *) install_prefix=$(pwd)/$install_prefix ;; # make absolute path
 175         esac
 176         ;;
 177
 178     --build-prefix) die "missing argument to $1 (try -h)" ;;
 179     --build-prefix=*) build_prefix=${1##*=} ;;
 180
 181     --name) die "missing argument to $1 (try -h)" ;;
 182     --name=*) build_name=${1##*=} ;;
 183
 184     --cadical) cadical=ON;;
 185     --no-cadical) cadical=OFF;;
 186
 187     --cln) cln=ON;;
 188     --no-cln) cln=OFF;;
 189
 190     --coverage) coverage=ON;;
 191     --no-coverage) coverage=OFF;;
 192
 193     --cryptominisat) cryptominisat=ON;;
 194     --no-cryptominisat) cryptominisat=OFF;;
 195
 196     --debug-symbols) debug_symbols=ON;;
 197     --no-debug-symbols) debug_symbols=OFF;;
 198
 199     --debug-context-memory-manager) debug_context_mm=ON;;
 200     --no-debug-context-memory-manager) debug_context_mm=OFF;;
 201
 202     --dumping) dumping=ON;;
 203     --no-dumping) dumping=OFF;;
 204
 205     --gpl) gpl=ON;;
 206     --no-gpl) gpl=OFF;;
 207
 208     --win64) win64=ON;;
 209     --no-win64) win64=OFF;;
 210
 211     --glpk) glpk=ON;;
 212     --no-glpk) glpk=OFF;;
 213
 214     --lfsc) lfsc=ON;;
 215     --no-lfsc) lfsc=OFF;;
 216
 217     --muzzle) muzzle=ON;;
 218     --no-muzzle) muzzle=OFF;;
 219
 220     --optimized) optimized=ON;;
 221     --no-optimized) optimized=OFF;;
 222
 223     --portfolio) portfolio=ON;;
 224     --no-portfolio) portfolio=OFF;;
 225
 226     --proofs) proofs=ON;;
 227     --no-proofs) proofs=OFF;;
 228
 229     --replay) replay=ON;;
 230     --no-replay) replay=OFF;;
 231
 232     --static) shared=OFF;;
 233     --no-static) shared=ON;;
 234
 235     --statistics) statistics=ON;;
 236     --no-statistics) statistics=OFF;;
 237
 238     --symfpu) symfpu=ON;;
 239     --no-symfpu) symfpu=OFF;;
 240
 241     --tracing) tracing=ON;;
 242     --no-tracing) tracing=OFF;;
 243
 244     --unit-testing) unit_testing=ON;;
 245     --no-unit-testing) unit_testing=OFF;;
 246
 247     --python2) python2=ON;;
 248     --no-python2) python2=OFF;;
 249
 250     --valgrind) valgrind=ON;;
 251     --no-valgrind) valgrind=OFF;;
 252
 253     --profiling) profiling=ON;;
 254     --no-profiling) profiling=OFF;;
 255
 256     --readline) readline=ON;;
 257     --no-readline) readline=OFF;;
 258
 259     --language-bindings) die "missing argument to $1 (try -h)" ;;
 260     --language-bindings=*)
 261       lang="${1##*=}"
 262       IFS=','
 263       for l in $lang; do
 264         case $l in
 265           java) language_bindings_java=ON ;;
 266           python) language_bindings_python=ON ;;
 267           all)
 268             language_bindings_python=ON
 269             language_bindings_java=ON ;;
 270           *) die "invalid language binding '$l' specified  (try -h)" ;;
 271         esac
 272       done
 273       unset IFS
 274       ;;
 275
 276     --abc-dir) die "missing argument to $1 (try -h)" ;;
 277     --abc-dir=*) abc_dir=${1##*=} ;;
 278
 279     --antlr-dir) die "missing argument to $1 (try -h)" ;;
 280     --antlr-dir=*) antlr_dir=${1##*=} ;;
 281
 282     --cadical-dir) die "missing argument to $1 (try -h)" ;;
 283     --cadical-dir=*) cadical_dir=${1##*=} ;;
 284
 285     --cryptominisat-dir) die "missing argument to $1 (try -h)" ;;
 286     --cryptominisat-dir=*) cryptominisat_dir=${1##*=} ;;
 287
 288     --glpk-dir) die "missing argument to $1 (try -h)" ;;
 289     --glpk-dir=*) glpk_dir=${1##*=} ;;
 290
 291     --gmp-dir) die "missing argument to $1 (try -h)" ;;
 292     --gmp-dir=*) gmp_dir=${1##*=} ;;
 293
 294     --lfsc-dir) die "missing argument to $1 (try -h)" ;;
 295     --lfsc-dir=*) lfsc_dir=${1##*=} ;;
 296
 297     --symfpu-dir) die "missing argument to $1 (try -h)" ;;
 298     --symfpu-dir=*) symfpu_dir=${1##*=} ;;
 299
 300     -*) die "invalid option '$1' (try -h)";;
 301
 302     *) case $1 in
 303          production)  buildtype=Production; build_dir=production;;
 304          debug)       buildtype=Debug; build_dir=debug;;
 305          testing)     buildtype=Testing; build_dir=testing;;
 306          competition) buildtype=Competition; build_dir=competition;;
 307          *)           die "invalid build type (try -h)";;
 308        esac
 309        ;;
 310   esac
 311   shift
 312 done
 313
 314 #--------------------------------------------------------------------------#
 315
 316 cmake_opts=""
 317
 318 [ $buildtype != default ] \
 319   && cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype"
 320
 321 [ $asan != default ] \
 322   && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan" \
 323   && [ $asan = ON ] && build_dir="$build_dir-asan"
 324 [ $assertions != default ] \
 325   && cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions" \
 326   && [ $assertions = ON ] && build_dir="$build_dir-assertions"
 327 [ $best != default ] \
 328   && cmake_opts="$cmake_opts -DENABLE_BEST=$best" \
 329   && [ $best = ON ] && build_dir="$build_dir-best"
 330 [ $coverage != default ] \
 331   && cmake_opts="$cmake_opts -DENABLE_COVERAGE=$coverage" \
 332   && [ $coverage = ON ] && build_dir="$build_dir-coverage"
 333 [ $debug_symbols != default ] \
 334   && cmake_opts="$cmake_opts -DENABLE_DEBUG_SYMBOLS=$debug_symbols" \
 335   && [ $debug_symbols = ON ] && build_dir="$build_dir-debug_symbols"
 336 [ $debug_context_mm != default ] \
 337   && cmake_opts="$cmake_opts -DENABLE_DEBUG_CONTEXT_MM=$debug_context_mm" \
 338   && [ $debug_context_mm = ON ] &&  build_dir="$build_dir-debug_context_mm"
 339 [ $dumping != default ] \
 340   && cmake_opts="$cmake_opts -DENABLE_DUMPING=$dumping" \
 341   && [ $dumping = ON ] &&  build_dir="$build_dir-dumping"
 342 [ $gpl != default ] \
 343   && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl" \
 344   && [ $gpl = ON ] &&  build_dir="$build_dir-gpl"
 345 [ $win64 != default ] \
 346   && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake" \
 347   && [ $win64 = ON ] &&  build_dir="$build_dir-win64"
 348 [ $muzzle != default ] \
 349   && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle" \
 350   && [ $muzzle = ON ] &&  build_dir="$build_dir-muzzle"
 351 [ $optimized != default ] \
 352   && cmake_opts="$cmake_opts -DENABLE_OPTIMIZED=$optimized" \
 353   && [ $optimized = ON ] &&  build_dir="$build_dir-optimized"
 354 [ $portfolio != default ] \
 355   && cmake_opts="$cmake_opts -DENABLE_PORTFOLIO=$portfolio" \
 356   && [ $portfolio = ON ] &&  build_dir="$build_dir-portfolio"
 357 [ $proofs != default ] \
 358   && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs" \
 359   && [ $proofs = ON ] &&  build_dir="$build_dir-proofs"
 360 [ $replay != default ] \
 361   && cmake_opts="$cmake_opts -DENABLE_REPLAY=$replay" \
 362   && [ $replay = ON ] &&  build_dir="$build_dir-replay"
 363 [ $shared != default ] \
 364   && cmake_opts="$cmake_opts -DENABLE_SHARED=$shared" \
 365   && [ $shared = OFF ] &&  build_dir="$build_dir-static"
 366 [ $statistics != default ] \
 367   && cmake_opts="$cmake_opts -DENABLE_STATISTICS=$statistics" \
 368   && [ $statistics = ON ] && build_dir="$build_dir-stastitics"
 369 [ $tracing != default ] \
 370   && cmake_opts="$cmake_opts -DENABLE_TRACING=$tracing" \
 371   && [ $tracing = ON ] && build_dir="$build_dir-tracing"
 372 [ $unit_testing != default ] \
 373   && cmake_opts="$cmake_opts -DENABLE_UNIT_TESTING=$unit_testing" \
 374   && [ $unit_testing = ON ] && build_dir="$build_dir-unit_testing"
 375 [ $python2 != default ] \
 376   && cmake_opts="$cmake_opts -DUSE_PYTHON2=$python2" \
 377   && [ $python2 = ON ] && build_dir="$build_dir-python2"
 378 [ $valgrind != default ] \
 379   && cmake_opts="$cmake_opts -DENABLE_VALGRIND=$valgrind" \
 380   && [ $valgrind = ON ] && build_dir="$build_dir-valgrind"
 381 [ $profiling != default ] \
 382   && cmake_opts="$cmake_opts -DENABLE_PROFILING=$profiling" \
 383   && [ $profiling = ON ] && build_dir="$build_dir-profiling"
 384 [ $readline != default ] \
 385   && cmake_opts="$cmake_opts -DUSE_READLINE=$readline" \
 386   && [ $readline = ON ] && build_dir="$build_dir-readline"
 387 [ $abc != default ] \
 388   && cmake_opts="$cmake_opts -DUSE_ABC=$abc" \
 389   && [ $abc = ON ] && build_dir="$build_dir-abc"
 390 [ $cadical != default ] \
 391   && cmake_opts="$cmake_opts -DUSE_CADICAL=$cadical" \
 392   && [ $cadical = ON ] && build_dir="$build_dir-cadical"
 393 [ $cln != default ] \
 394   && cmake_opts="$cmake_opts -DUSE_CLN=$cln" \
 395   && [ $cln = ON ] && build_dir="$build_dir-cln"
 396 [ $cryptominisat != default ] \
 397   && cmake_opts="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat" \
 398   && [ $cryptominisat = ON ] && build_dir="$build_dir-cryptominisat"
 399 [ $glpk != default ] \
 400   && cmake_opts="$cmake_opts -DUSE_GLPK=$glpk" \
 401   && [ $glpk = ON ] && build_dir="$build_dir-glpk"
 402 [ $lfsc != default ] \
 403   && cmake_opts="$cmake_opts -DUSE_LFSC=$lfsc" \
 404   && [ $lfsc = ON ] && build_dir="$build_dir-lfsc"
 405 [ $symfpu != default ] \
 406   && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu" \
 407   && [ $symfpu = ON ] && build_dir="$build_dir-symfpu"
 408
 409 [ $language_bindings_java != default ] \
 410   && cmake_opts="$cmake_opts -DBUILD_BINDINGS_JAVA=$language_bindings_java"
 411 [ $language_bindings_python != default ] \
 412   && cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$language_bindings_python"
 413
 414 [ "$abc_dir" != default ] \
 415   && cmake_opts="$cmake_opts -DABC_DIR=$abc_dir"
 416 [ "$antlr_dir" != default ] \
 417   && cmake_opts="$cmake_opts -DANTLR_DIR=$antlr_dir"
 418 [ "$cadical_dir" != default ] \
 419   && cmake_opts="$cmake_opts -DCADICAL_DIR=$cadical_dir"
 420 [ "$cryptominisat_dir" != default ] \
 421   && cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir"
 422 [ "$glpk_dir" != default ] \
 423   && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir"
 424 [ "$gmp_dir" != default ] \
 425   && cmake_opts="$cmake_opts -DGMP_DIR=$gmp_dir"
 426 [ "$lfsc_dir" != default ] \
 427   && cmake_opts="$cmake_opts -DLFSC_DIR=$lfsc_dir"
 428 [ "$symfpu_dir" != default ] \
 429   && cmake_opts="$cmake_opts -DSYMFPU_DIR=$symfpu_dir"
 430 [ "$install_prefix" != default ] \
 431   && cmake_opts="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix"
 432
 433 root_dir=$(pwd)
 434
 435 if [ -n "$build_name" ]; then
 436   # If a build name is specified just create directory 'build_name' for the
 437   # current build.
 438   build_dir=$build_name
 439
 440   # The cmake toolchain can't be changed once it is configured in $build_dir.
 441   # Thus, remove $build_dir and create an empty directory.
 442   [ $win64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir"
 443   mkdir -p "$build_name"
 444 else
 445   # If no build name is specified create 'cmake-builds' directory and create
 446   # the current build directory. Set symlink 'cmake-builds/build/' to current
 447   # build.
 448   build_dir="$build_prefix$build_dir"
 449
 450   # The cmake toolchain can't be changed once it is configured in $build_dir.
 451   # Thus, remove $build_dir and create an empty directory.
 452   [ $win64 = ON ] && [ -e "cmake-build/$build_dir" ] \
 453     && rm -r "cmake-builds/$build_dir"
 454   mkdir -p "cmake-builds/$build_dir"
 455   cd cmake-builds || exit 1
 456   [ -e build ] && rm build
 457   ln -s "$build_dir" build  # link to current build directory
 458 fi
 459
 460 cd "$build_dir" || exit 1
 461
 462 [ -e CMakeCache.txt ] && rm CMakeCache.txt
 463 cmake "$root_dir" $cmake_opts