configure.sh

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