[proofs] Make sure --proof-check=... is no-op when not checking proofs (#7638)
[cvc5.git] / 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 and options known to give best performance
24 --gpl permit GPL dependencies, if available
25 --arm64 cross-compile for Linux ARM 64 bit
26 --win64 cross-compile for Windows 64 bit
27 --ninja use Ninja build system
28 --docs build Api documentation
29
30
31 Features:
32 The following flags enable optional features (disable with --no-<option name>).
33 --static build static libraries and binaries [default=no]
34 --auto-download automatically download dependencies if necessary
35 --debug-symbols include debug symbols
36 --valgrind Valgrind instrumentation
37 --debug-context-mm use the debug context memory manager
38 --statistics include statistics
39 --assertions turn on assertions
40 --tracing include tracing code
41 --dumping include dumping code
42 --muzzle complete silence (no non-result output)
43 --coverage support for gcov coverage testing
44 --profiling support for gprof profiling
45 --unit-testing support for unit testing
46 --python2 force Python 2 (deprecated)
47 --python-bindings build Python bindings based on new C++ API
48 --java-bindings build Java bindings based on new C++ API
49 --all-bindings build bindings for all supported languages
50 --asan build with ASan instrumentation
51 --ubsan build with UBSan instrumentation
52 --tsan build with TSan instrumentation
53 --werror build with -Werror
54 --ipo build with interprocedural optimization
55
56 Optional Packages:
57 The following flags enable optional packages (disable with --no-<option name>).
58 --cln use CLN instead of GMP
59 --glpk use GLPK simplex solver
60 --cryptominisat use the CryptoMiniSat SAT solver
61 --kissat use the Kissat SAT solver
62 --poly use the LibPoly library [default=yes]
63 --cocoa use the CoCoA library
64 --editline support the editline library
65
66 Optional Path to Optional Packages:
67 --glpk-dir=PATH path to top level of GLPK installation
68 --dep-path=PATH path to a dependency installation dir
69
70 Build limitations:
71 --lib-only only build the library, but not the executable or
72 the parser (default: off)
73
74 CMake Options (Advanced)
75 -DVAR=VALUE manually add CMake options
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 asan=default
107 assertions=default
108 auto_download=default
109 cln=default
110 comp_inc=default
111 coverage=default
112 cryptominisat=default
113 debug_context_mm=default
114 debug_symbols=default
115 docs=default
116 dumping=default
117 glpk=default
118 gpl=default
119 kissat=default
120 poly=ON
121 cocoa=default
122 muzzle=default
123 ninja=default
124 profiling=default
125 python2=default
126 python_bindings=default
127 java_bindings=default
128 editline=default
129 build_shared=ON
130 statistics=default
131 tracing=default
132 tsan=default
133 ubsan=default
134 unit_testing=default
135 valgrind=default
136 win64=default
137 arm64=default
138 werror=default
139 ipo=default
140
141 glpk_dir=default
142
143 #--------------------------------------------------------------------------#
144
145 cmake_opts=""
146
147 while [ $# -gt 0 ]
148 do
149 case $1 in
150
151 -h|--help) usage;;
152
153 --asan) asan=ON;;
154 --no-asan) asan=OFF;;
155
156 --ubsan) ubsan=ON;;
157 --no-ubsan) ubsan=OFF;;
158
159 --tsan) tsan=ON;;
160 --no-tsan) tsan=OFF;;
161
162 --werror) werror=ON;;
163
164 --ipo) ipo=ON;;
165 --no-ipo) ipo=OFF;;
166
167 --assertions) assertions=ON;;
168 --no-assertions) assertions=OFF;;
169
170 # Best configuration
171 --best)
172 ipo=ON
173 cln=ON
174 cryptominisat=ON
175 glpk=ON
176 editline=ON
177 ;;
178
179 --prefix) die "missing argument to $1 (try -h)" ;;
180 --prefix=*)
181 install_prefix=${1##*=}
182 # Check if install_prefix is an absolute path and if not, make it
183 # absolute.
184 case $install_prefix in
185 /*) ;; # absolute path
186 *) install_prefix=$(pwd)/$install_prefix ;; # make absolute path
187 esac
188 ;;
189
190 --program-prefix) die "missing argument to $1 (try -h)" ;;
191 --program-prefix=*) program_prefix=${1##*=} ;;
192
193 --name) die "missing argument to $1 (try -h)" ;;
194 --name=*) build_dir=${1##*=} ;;
195
196 --cln) cln=ON;;
197 --no-cln) cln=OFF;;
198
199 --coverage) coverage=ON;;
200 --no-coverage) coverage=OFF;;
201
202 --cryptominisat) cryptominisat=ON;;
203 --no-cryptominisat) cryptominisat=OFF;;
204
205 --debug-symbols) debug_symbols=ON;;
206 --no-debug-symbols) debug_symbols=OFF;;
207
208 --debug-context-mm) debug_context_mm=ON;;
209 --no-debug-context-mm) debug_context_mm=OFF;;
210
211 --dumping) dumping=ON;;
212 --no-dumping) dumping=OFF;;
213
214 --gpl) gpl=ON;;
215 --no-gpl) gpl=OFF;;
216
217 --kissat) kissat=ON;;
218 --no-kissat) kissat=OFF;;
219
220 --win64) win64=ON;;
221
222 --arm64) arm64=ON;;
223
224 --ninja) ninja=ON;;
225
226 --docs) docs=ON;;
227 --no-docs) docs=OFF;;
228
229 --glpk) glpk=ON;;
230 --no-glpk) glpk=OFF;;
231
232 --poly) poly=ON;;
233 --no-poly) poly=OFF;;
234
235 --cocoa) cocoa=ON;;
236 --no-cocoa) cocoa=OFF;;
237
238 --muzzle) muzzle=ON;;
239 --no-muzzle) muzzle=OFF;;
240
241 --static) build_shared=OFF;;
242 --no-static) build_shared=ON;;
243
244 --auto-download) auto_download=ON;;
245 --no-auto-download) auto_download=OFF;;
246
247 --statistics) statistics=ON;;
248 --no-statistics) statistics=OFF;;
249
250 --tracing) tracing=ON;;
251 --no-tracing) tracing=OFF;;
252
253 --unit-testing) unit_testing=ON;;
254 --no-unit-testing) unit_testing=OFF;;
255
256 --python2) python2=ON;;
257 --no-python2) python2=OFF;;
258
259 --python-bindings) python_bindings=ON;;
260 --no-python-bindings) python_bindings=OFF;;
261
262 --java-bindings) java_bindings=ON;;
263 --no-java-bindings) java_bindings=OFF;;
264
265 --all-bindings)
266 python_bindings=ON
267 java_bindings=ON;;
268
269 --valgrind) valgrind=ON;;
270 --no-valgrind) valgrind=OFF;;
271
272 --profiling) profiling=ON;;
273 --no-profiling) profiling=OFF;;
274
275 --editline) editline=ON;;
276 --no-editline) editline=OFF;;
277
278 --glpk-dir) die "missing argument to $1 (try -h)" ;;
279 --glpk-dir=*) glpk_dir=${1##*=} ;;
280
281 --dep-path) die "missing argument to $1 (try -h)" ;;
282 --dep-path=*) dep_path="${dep_path};${1##*=}" ;;
283
284 -D*) cmake_opts="${cmake_opts} $1" ;;
285
286 -*) die "invalid option '$1' (try -h)";;
287
288 *) case $1 in
289 production) buildtype=Production;;
290 debug) buildtype=Debug;;
291 testing) buildtype=Testing;;
292 competition) buildtype=Competition;;
293 competition-inc) buildtype=Competition; comp_inc=ON;;
294 *) die "invalid build type (try -h)";;
295 esac
296 ;;
297 esac
298 shift
299 done
300
301 #--------------------------------------------------------------------------#
302
303 if [ $werror != default ]; then
304 export CFLAGS=-Werror
305 export CXXFLAGS=-Werror
306 fi
307
308 [ $buildtype != default ] \
309 && cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype"
310
311 [ $asan != default ] \
312 && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan"
313 [ $auto_download != default ] \
314 && cmake_opts="$cmake_opts -DENABLE_AUTO_DOWNLOAD=$auto_download"
315 [ $ubsan != default ] \
316 && cmake_opts="$cmake_opts -DENABLE_UBSAN=$ubsan"
317 [ $tsan != default ] \
318 && cmake_opts="$cmake_opts -DENABLE_TSAN=$tsan"
319 [ $ipo != default ] \
320 && cmake_opts="$cmake_opts -DENABLE_IPO=$ipo"
321 [ $assertions != default ] \
322 && cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions"
323 [ $comp_inc != default ] \
324 && cmake_opts="$cmake_opts -DENABLE_COMP_INC_TRACK=$comp_inc"
325 [ $coverage != default ] \
326 && cmake_opts="$cmake_opts -DENABLE_COVERAGE=$coverage"
327 [ $debug_symbols != default ] \
328 && cmake_opts="$cmake_opts -DENABLE_DEBUG_SYMBOLS=$debug_symbols"
329 [ $debug_context_mm != default ] \
330 && cmake_opts="$cmake_opts -DENABLE_DEBUG_CONTEXT_MM=$debug_context_mm"
331 [ $dumping != default ] \
332 && cmake_opts="$cmake_opts -DENABLE_DUMPING=$dumping"
333 [ $gpl != default ] \
334 && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl"
335 [ $win64 != default ] \
336 && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake"
337 [ $arm64 != default ] \
338 && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-aarch64.cmake"
339 [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
340 [ $muzzle != default ] \
341 && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
342 [ $build_shared != default ] \
343 && cmake_opts="$cmake_opts -DBUILD_SHARED_LIBS=$build_shared"
344 [ $statistics != default ] \
345 && cmake_opts="$cmake_opts -DENABLE_STATISTICS=$statistics"
346 [ $tracing != default ] \
347 && cmake_opts="$cmake_opts -DENABLE_TRACING=$tracing"
348 [ $unit_testing != default ] \
349 && cmake_opts="$cmake_opts -DENABLE_UNIT_TESTING=$unit_testing"
350 [ $python2 != default ] \
351 && cmake_opts="$cmake_opts -DUSE_PYTHON2=$python2"
352 [ $docs != default ] \
353 && cmake_opts="$cmake_opts -DBUILD_DOCS=$docs"
354 [ $python_bindings != default ] \
355 && cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$python_bindings"
356 [ $java_bindings != default ] \
357 && cmake_opts="$cmake_opts -DBUILD_BINDINGS_JAVA=$java_bindings"
358 [ $valgrind != default ] \
359 && cmake_opts="$cmake_opts -DENABLE_VALGRIND=$valgrind"
360 [ $profiling != default ] \
361 && cmake_opts="$cmake_opts -DENABLE_PROFILING=$profiling"
362 [ $editline != default ] \
363 && cmake_opts="$cmake_opts -DUSE_EDITLINE=$editline"
364 [ $cln != default ] \
365 && cmake_opts="$cmake_opts -DUSE_CLN=$cln"
366 [ $cryptominisat != default ] \
367 && cmake_opts="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat"
368 [ $glpk != default ] \
369 && cmake_opts="$cmake_opts -DUSE_GLPK=$glpk"
370 [ $kissat != default ] \
371 && cmake_opts="$cmake_opts -DUSE_KISSAT=$kissat"
372 [ $poly != default ] \
373 && cmake_opts="$cmake_opts -DUSE_POLY=$poly"
374 [ $cocoa != default ] \
375 && cmake_opts="$cmake_opts -DUSE_COCOA=$cocoa"
376 [ "$glpk_dir" != default ] \
377 && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir"
378 [ "$dep_path" != default ] \
379 && cmake_opts="$cmake_opts -DCMAKE_PREFIX_PATH=$dep_path"
380 [ "$install_prefix" != default ] \
381 && cmake_opts="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix"
382 [ -n "$program_prefix" ] \
383 && cmake_opts="$cmake_opts -DPROGRAM_PREFIX=$program_prefix"
384
385 root_dir=$(pwd)
386
387 # The cmake toolchain can't be changed once it is configured in $build_dir.
388 # Thus, remove $build_dir and create an empty directory.
389 [ $win64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir"
390 [ $arm64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir"
391 mkdir -p "$build_dir"
392
393 cd "$build_dir"
394
395 [ -e CMakeCache.txt ] && rm CMakeCache.txt
396 build_dir_escaped=$(echo "$build_dir" | sed 's/\//\\\//g')
397 cmake "$root_dir" $cmake_opts 2>&1 | \
398 sed "s/^Now just/Now change to '$build_dir_escaped' and/"