-#!/bin/sh
+#!/bin/bash
#--------------------------------------------------------------------------#
+set -e -o pipefail
+
usage () {
cat <<EOF
-Usage: VAR=VALUE $0 [<build type>] [<option> ...]
+Usage: $0 [<build type>] [<option> ...]
Build types:
production
debug
testing
competition
+ competition-inc
General options;
-h, --help display this help and exit
- --gpl permit GPL dependences, if available
- --best turn on dependences known to give best performance
+ --prefix=STR install directory
+ --program-prefix=STR prefix of binaries prepended on make install
+ --name=STR use custom build directory name (optionally: +path)
+ --best turn on dependencies known to give best performance
+ --gpl permit GPL dependencies, if available
+ --arm64 cross-compile for Linux ARM 64 bit
+ --win64 cross-compile for Windows 64 bit
+ --ninja use Ninja build system
+ --docs build Api documentation
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
+ --static-binary statically link against system libraries
+ (must be disabled for static macOS builds) [default=yes]
+ --auto-download automatically download dependencies if necessary
--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
+ --statistics include statistics
+ --assertions turn on assertions
+ --tracing include tracing code
+ --dumping include 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.
-
- --language-bindings[=c,c++,java,all]
- specify language bindings to build
+ --python2 force Python 2 (deprecated)
+ --python-bindings build Python bindings based on new C++ API
+ --java-bindings build Java bindings based on new C++ API
+ --all-bindings build bindings for all supported languages
+ --asan build with ASan instrumentation
+ --ubsan build with UBSan instrumentation
+ --tsan build with TSan instrumentation
+ --werror build with -Werror
Optional Packages:
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
+ --cryptominisat use the CryptoMiniSat SAT solver
+ --kissat use the Kissat SAT solver
+ --poly use the LibPoly library [default=yes]
+ --cocoa use the CoCoA library
+ --editline support the editline 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>.
+ --abc-dir=PATH path to top level of ABC source tree
+ --glpk-dir=PATH path to top level of GLPK installation
+ --dep-path=PATH path to a dependency installation dir
+
+Build limitations:
+ --lib-only only build the library, but not the executable or
+ the parser (default: off)
+
+CMake Options (Advanced)
+ -DVAR=VALUE manually add CMake options
+
EOF
exit 0
}
-#To assign environment variables (e.g., CC, CFLAGS...), specify them as
-#VAR=VALUE. See below for descriptions of some of the useful variables.
-#
-#Some influential environment variables:
-# CXX C++ compiler command
-# CXXFLAGS C++ compiler flags
-# LDFLAGS linker flags, e.g. -L<lib dir> if you have libraries in a
-# nonstandard directory <lib dir>
-# LIBS libraries to pass to the linker, e.g. -l<library>
-# CPPFLAGS (Objective) C/C++ preprocessor flags, e.g. -I<include dir> if
-# you have headers in a nonstandard directory <include dir>
-# CC C compiler command
-# CFLAGS C compiler flags
-# LT_SYS_LIBRARY_PATH
-# User-defined run-time library search path.
-# CPP C preprocessor
-# CXXCPP C++ preprocessor
-# PKG_CONFIG path to pkg-config utility
-# CLN_CFLAGS C compiler flags for CLN, overriding pkg-config
-# CLN_LIBS linker flags for CLN, overriding pkg-config
-# GLPK_HOME path to top level of glpk installation
-# ABC_HOME path to top level of abc source tree
-# CADICAL_HOME
-# path to top level of CaDiCaL source tree
-# CRYPTOMINISAT_HOME
-# path to top level of cryptominisat source tree
-# LFSC_HOME path to top level of LFSC source tree
-# SYMFPU_HOME path to top level of symfpu source tree
-# ANTLR location of the antlr3 script
-# DOXYGEN_PAPER_SIZE
-# a4wide (default), a4, letter, legal or executive
-# CXXTEST path to CxxTest installation
-# TEST_CPPFLAGS
-# CPPFLAGS to use when testing (default=$CPPFLAGS)
-# TEST_CXXFLAGS
-# CXXFLAGS to use when testing (default=$CXXFLAGS)
-# TEST_LDFLAGS
-# LDFLAGS to use when testing (default=$LDFLAGS)
-# PERL PERL interpreter (used when testing)
-# PYTHON the Python interpreter
-# ANTLR_HOME path to libantlr3c installation
-# SWIG SWIG binary (used to generate language bindings)
-# JAVA_CPPFLAGS
-# flags to pass to compiler when building Java bindings
-# CSHARP_CPPFLAGS
-# flags to pass to compiler when building C# bindings
-# PERL_CPPFLAGS
-# flags to pass to compiler when building perl bindings
-# PHP_CPPFLAGS
-# flags to pass to compiler when building PHP bindings
-# PYTHON_INCLUDE
-# Include flags for python, bypassing python-config
-# PYTHON_CONFIG
-# Path to python-config
-# RUBY_CPPFLAGS
-# flags to pass to compiler when building ruby bindings
-# TCL_CPPFLAGS
-# flags to pass to compiler when building tcl bindings
-# OCAMLC OCaml compiler
-# OCAMLMKTOP OCaml runtime-maker
-# OCAMLFIND OCaml-find binary
-# CAMLP4O camlp4o binary
-# BOOST_ROOT Location of Boost installation
-# JAVA Java interpreter (used when testing Java interface)
-# JAVAC Java compiler (used when building and testing Java interface)
-# JAVAH Java compiler (used when building and testing Java interface)
-# JAR Jar archiver (used when building Java interface)
-#
-#Use these variables to override the choices made by `configure' or to help
-#it to find libraries and programs with nonstandard names/locations.
-
-
#--------------------------------------------------------------------------#
die () {
#--------------------------------------------------------------------------#
-BUILDDIR=build
+build_dir=build
+install_prefix=default
+program_prefix=""
#--------------------------------------------------------------------------#
abc=default
asan=default
assertions=default
-best=default
-cadical=default
+auto_download=default
cln=default
+comp_inc=default
coverage=default
cryptominisat=default
-debug_symbols=default
debug_context_mm=default
+debug_symbols=default
+docs=default
dumping=default
-gpl=default
glpk=default
-lfsc=default
+gpl=default
+kissat=default
+poly=ON
+cocoa=default
muzzle=default
-optimized=default
-portfolio=default
-proofs=default
-replay=default
-static=default
+ninja=default
+profiling=default
+python2=default
+python_bindings=default
+java_bindings=default
+editline=default
+shared=default
+static_binary=default
statistics=default
-symfpu=default
tracing=default
+tsan=default
+ubsan=default
unit_testing=default
valgrind=default
-profiling=default
-readline=default
-
-language_bindings=default
+win64=default
+arm64=default
+werror=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
+
+lib_only=default
#--------------------------------------------------------------------------#
+cmake_opts=""
+
while [ $# -gt 0 ]
do
case $1 in
--asan) asan=ON;;
--no-asan) asan=OFF;;
+ --ubsan) ubsan=ON;;
+ --no-ubsan) ubsan=OFF;;
+
+ --tsan) tsan=ON;;
+ --no-tsan) tsan=OFF;;
+
+ --werror) werror=ON;;
+
--assertions) assertions=ON;;
--no-assertions) assertions=OFF;;
- --best) best=ON;;
- --no-best) best=OFF;;
+ # Best configuration
+ --best)
+ abc=ON
+ cln=ON
+ cryptominisat=ON
+ glpk=ON
+ editline=ON
+ ;;
+
+ --prefix) die "missing argument to $1 (try -h)" ;;
+ --prefix=*)
+ install_prefix=${1##*=}
+ # Check if install_prefix is an absolute path and if not, make it
+ # absolute.
+ case $install_prefix in
+ /*) ;; # absolute path
+ *) install_prefix=$(pwd)/$install_prefix ;; # make absolute path
+ esac
+ ;;
- --cadical) cadical=ON;;
- --no-cadical) cadical=OFF;;
+ --program-prefix) die "missing argument to $1 (try -h)" ;;
+ --program-prefix=*) program_prefix=${1##*=} ;;
+
+ --name) die "missing argument to $1 (try -h)" ;;
+ --name=*) build_dir=${1##*=} ;;
--cln) cln=ON;;
--no-cln) cln=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;;
+ --debug-context-mm) debug_context_mm=ON;;
+ --no-debug-context-mm) debug_context_mm=OFF;;
--dumping) dumping=ON;;
--no-dumping) dumping=OFF;;
--gpl) gpl=ON;;
--no-gpl) gpl=OFF;;
+ --kissat) kissat=ON;;
+ --no-kissat) kissat=OFF;;
+
+ --win64) win64=ON;;
+
+ --arm64) arm64=ON;;
+
+ --ninja) ninja=ON;;
+
+ --docs) docs=ON;;
+ --no-docs) docs=OFF;;
+
--glpk) glpk=ON;;
--no-glpk) glpk=OFF;;
- --lfsc) lfsc=ON;;
- --no-lfsc) lfsc=OFF;;
+ --poly) poly=ON;;
+ --no-poly) poly=OFF;;
+
+ --cocoa) cocoa=ON;;
+ --no-cocoa) cocoa=OFF;;
--muzzle) muzzle=ON;;
--no-muzzle) muzzle=OFF;;
- --optimized) optimized=ON;;
- --no-optimized) optimized=OFF;;
+ --static) shared=OFF; static_binary=ON;;
+ --no-static) shared=ON;;
- --portfolio) portfolio=ON;;
- --no-portfolio) portfolio=OFF;;
+ --static-binary) static_binary=ON;;
+ --no-static-binary) static_binary=OFF;;
- --proofs) proofs=ON;;
- --no-proofs) proofs=OFF;;
-
- --replay) replay=ON;;
- --no-replay) replay=OFF;;
-
- --static) static=ON;;
- --no-static) static=OFF;;
+ --auto-download) auto_download=ON;;
+ --no-auto-download) auto_download=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;;
+ --python2) python2=ON;;
+ --no-python2) python2=OFF;;
+
+ --python-bindings) python_bindings=ON;;
+ --no-python-bindings) python_bindings=OFF;;
+
+ --java-bindings) java_bindings=ON;;
+ --no-java-bindings) java_bindings=OFF;;
+
+ --all-bindings)
+ python_bindings=ON
+ java_bindings=ON;;
+
--valgrind) valgrind=ON;;
--no-valgrind) valgrind=OFF;;
--profiling) profiling=ON;;
--no-profiling) profiling=OFF;;
- --readline) readline=ON;;
- --no-readline) readline=OFF;;
-
- --language-bindings)
- shift
- if [ $# -eq 0 ]
- then
- die "missing argument to --language-bindings-dir"
- fi
- [[ "c c++ java all" =~ (^|[[:space:]])"$1"($|[[:space:]]) ]] \
- || die "invalid argument to --language-bindings (try '-h')"
- language_bindings=$1
- ;;
+ --editline) editline=ON;;
+ --no-editline) editline=OFF;;
- --abc-dir)
- shift
- if [ $# -eq 0 ]
- then
- die "missing argument to --abc-dir"
- fi
- abc_dir=$1
- ;;
- --antlr-dir)
- shift
- if [ $# -eq 0 ]
- then
- die "missing argument to --antlr-dir"
- fi
- antlr_dir=$1
- ;;
- --cadical-dir)
- shift
- if [ $# -eq 0 ]
- then
- die "missing argument to --cadical-dir"
- fi
- cadical_dir=$1
- ;;
- --cryptominisat-dir)
- shift
- if [ $# -eq 0 ]
- then
- die "missing argument to --cryptominisat-dir"
- fi
- cryptominisat_dir=$1
- ;;
- --cxxtest-dir)
- shift
- if [ $# -eq 0 ]
- then
- die "missing argument to --cxxtest-dir"
- fi
- cxxtest_dir=$1
- ;;
- --glpk-dir)
- shift
- if [ $# -eq 0 ]
- then
- die "missing argument to --glpk-dir"
- fi
- glpk_dir=$1
- ;;
- --lfsc-dir)
- shift
- if [ $# -eq 0 ]
- then
- die "missing argument to --lfsc-dir"
- fi
- lfsc_dir=$1
- ;;
- --symfpu-dir)
- shift
- if [ $# -eq 0 ]
- then
- die "missing argument to --symfpu-dir"
- fi
- symfpu_dir=$1
- ;;
+ --abc-dir) die "missing argument to $1 (try -h)" ;;
+ --abc-dir=*) abc_dir=${1##*=} ;;
+
+ --glpk-dir) die "missing argument to $1 (try -h)" ;;
+ --glpk-dir=*) glpk_dir=${1##*=} ;;
+
+ --dep-path) die "missing argument to $1 (try -h)" ;;
+ --dep-path=*) dep_path="${dep_path};${1##*=}" ;;
- -*) die "invalid option '$1' (try '-h')";;
+ --lib-only) lib_only=ON ;;
+ -D*) cmake_opts="${cmake_opts} $1" ;;
+
+ -*) die "invalid option '$1' (try -h)";;
*) case $1 in
- production) buildtype=Production;;
- debug) buildtype=Debug;;
- testing) buildtype=Testing;;
- competition) buildtype=Competition;;
- *) die "invalid build type (try '-h')";;
+ production) buildtype=Production;;
+ debug) buildtype=Debug;;
+ testing) buildtype=Testing;;
+ competition) buildtype=Competition;;
+ competition-inc) buildtype=Competition; comp_inc=ON;;
+ *) die "invalid build type (try -h)";;
esac
;;
esac
#--------------------------------------------------------------------------#
-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
+if [ $werror != default ]; then
+ export CFLAGS=-Werror
+ export CXXFLAGS=-Werror
+fi
+
+[ $buildtype != default ] \
+ && cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype"
+
+[ $asan != default ] \
+ && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan"
+[ $auto_download != default ] \
+ && cmake_opts="$cmake_opts -DENABLE_AUTO_DOWNLOAD=$auto_download"
+[ $ubsan != default ] \
+ && cmake_opts="$cmake_opts -DENABLE_UBSAN=$ubsan"
+[ $tsan != default ] \
+ && cmake_opts="$cmake_opts -DENABLE_TSAN=$tsan"
+[ $assertions != default ] \
+ && cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions"
+[ $comp_inc != default ] \
+ && cmake_opts="$cmake_opts -DENABLE_COMP_INC_TRACK=$comp_inc"
+[ $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"
+[ $win64 != default ] \
+ && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake"
+[ $arm64 != default ] \
+ && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-aarch64.cmake"
+[ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
+[ $muzzle != default ] \
+ && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
+[ $shared != default ] \
+ && cmake_opts="$cmake_opts -DENABLE_SHARED=$shared"
+[ $static_binary != default ] \
+ && cmake_opts="$cmake_opts -DENABLE_STATIC_BINARY=$static_binary"
+[ $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"
+[ $python2 != default ] \
+ && cmake_opts="$cmake_opts -DUSE_PYTHON2=$python2"
+[ $docs != default ] \
+ && cmake_opts="$cmake_opts -DBUILD_DOCS=$docs"
+[ $python_bindings != default ] \
+ && cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$python_bindings"
+[ $java_bindings != default ] \
+ && cmake_opts="$cmake_opts -DBUILD_BINDINGS_JAVA=$java_bindings"
+[ $valgrind != default ] \
+ && cmake_opts="$cmake_opts -DENABLE_VALGRIND=$valgrind"
+[ $profiling != default ] \
+ && cmake_opts="$cmake_opts -DENABLE_PROFILING=$profiling"
+[ $editline != default ] \
+ && cmake_opts="$cmake_opts -DUSE_EDITLINE=$editline"
+[ $abc != default ] \
+ && cmake_opts="$cmake_opts -DUSE_ABC=$abc"
+[ $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"
+[ $kissat != default ] \
+ && cmake_opts="$cmake_opts -DUSE_KISSAT=$kissat"
+[ $poly != default ] \
+ && cmake_opts="$cmake_opts -DUSE_POLY=$poly"
+[ $cocoa != default ] \
+ && cmake_opts="$cmake_opts -DUSE_COCOA=$cocoa"
+[ "$abc_dir" != default ] \
+ && cmake_opts="$cmake_opts -DABC_DIR=$abc_dir"
+[ "$glpk_dir" != default ] \
+ && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir"
+[ "$dep_path" != default ] \
+ && cmake_opts="$cmake_opts -DCMAKE_PREFIX_PATH=$dep_path"
+[ "$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" ] \
+ && cmake_opts="$cmake_opts -DPROGRAM_PREFIX=$program_prefix"
+
+root_dir=$(pwd)
+
+# The cmake toolchain can't be changed once it is configured in $build_dir.
+# Thus, remove $build_dir and create an empty directory.
+[ $win64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir"
+[ $arm64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir"
+mkdir -p "$build_dir"
+
+cd "$build_dir"
[ -e CMakeCache.txt ] && rm CMakeCache.txt
-cmake .. $cmake_opts
+build_dir_escaped=$(echo "$build_dir" | sed 's/\//\\\//g')
+cmake "$root_dir" $cmake_opts 2>&1 | \
+ sed "s/^Now just/Now change to '$build_dir_escaped' and/"
projects / cvc5.git / blobdiff