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