Expand arith's farkas lemma rule as a macro (#6577)
[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 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 --static-binary statically link against system libraries
35 (must be disabled for static macOS builds) [default=yes]
36 --auto-download automatically download dependencies if necessary
37 --debug-symbols include debug symbols
38 --valgrind Valgrind instrumentation
39 --debug-context-mm use the debug context memory manager
40 --statistics include statistics
41 --assertions turn on assertions
42 --tracing include tracing code
43 --dumping include dumping code
44 --muzzle complete silence (no non-result output)
45 --coverage support for gcov coverage testing
46 --profiling support for gprof profiling
47 --unit-testing support for unit testing
48 --python2 force Python 2 (deprecated)
49 --python-bindings build Python bindings based on new C++ API
50 --java-bindings build Java bindings based on new C++ API
51 --all-bindings build bindings for all supported languages
52 --asan build with ASan instrumentation
53 --ubsan build with UBSan instrumentation
54 --tsan build with TSan instrumentation
55 --werror build with -Werror
56
57 Optional Packages:
58 The following flags enable optional packages (disable with --no-<option name>).
59 --cln use CLN instead of GMP
60 --glpk use GLPK simplex solver
61 --abc use the ABC AIG library
62 --cadical use the CaDiCaL SAT solver [default=yes]
63 --cryptominisat use the CryptoMiniSat SAT solver
64 --kissat use the Kissat SAT solver
65 --poly use the LibPoly library [default=yes]
66 --symfpu use SymFPU for floating point solver [default=yes]
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 --glpk-dir=PATH path to top level of GLPK installation
72 --dep-path=PATH path to a dependency installation dir
73
74 Build limitations:
75 --lib-only only build the library, but not the executable or
76 the parser (default: off)
77
78 EOF
79 exit 0
80 }
81
82 #--------------------------------------------------------------------------#
83
84 die () {
85 echo "*** configure.sh: $*" 1>&2
86 exit 1
87 }
88
89 msg () {
90 echo "[configure.sh] $*"
91 }
92
93 #--------------------------------------------------------------------------#
94
95 [ ! -e src/theory ] && die "$0 not called from CVC4 base directory"
96
97 #--------------------------------------------------------------------------#
98
99 build_dir=build
100 install_prefix=default
101 program_prefix=""
102
103 #--------------------------------------------------------------------------#
104
105 buildtype=default
106
107 abc=default
108 asan=default
109 assertions=default
110 auto_download=default
111 cadical=ON
112 cln=default
113 comp_inc=default
114 coverage=default
115 cryptominisat=default
116 debug_context_mm=default
117 debug_symbols=default
118 docs=default
119 dumping=default
120 glpk=default
121 gpl=default
122 kissat=default
123 poly=ON
124 muzzle=default
125 ninja=default
126 profiling=default
127 python2=default
128 python_bindings=default
129 java_bindings=default
130 editline=default
131 shared=default
132 static_binary=default
133 statistics=default
134 symfpu=ON
135 tracing=default
136 tsan=default
137 ubsan=default
138 unit_testing=default
139 valgrind=default
140 win64=default
141 arm64=default
142 werror=default
143
144 abc_dir=default
145 glpk_dir=default
146
147 lib_only=default
148
149 #--------------------------------------------------------------------------#
150
151 while [ $# -gt 0 ]
152 do
153 case $1 in
154
155 -h|--help) usage;;
156
157 --abc) abc=ON;;
158 --no-abc) abc=OFF;;
159
160 --asan) asan=ON;;
161 --no-asan) asan=OFF;;
162
163 --ubsan) ubsan=ON;;
164 --no-ubsan) ubsan=OFF;;
165
166 --tsan) tsan=ON;;
167 --no-tsan) tsan=OFF;;
168
169 --werror) werror=ON;;
170
171 --assertions) assertions=ON;;
172 --no-assertions) assertions=OFF;;
173
174 # Best configuration
175 --best)
176 abc=ON
177 cadical=ON
178 cln=ON
179 cryptominisat=ON
180 glpk=ON
181 editline=ON
182 ;;
183
184 --prefix) die "missing argument to $1 (try -h)" ;;
185 --prefix=*)
186 install_prefix=${1##*=}
187 # Check if install_prefix is an absolute path and if not, make it
188 # absolute.
189 case $install_prefix in
190 /*) ;; # absolute path
191 *) install_prefix=$(pwd)/$install_prefix ;; # make absolute path
192 esac
193 ;;
194
195 --program-prefix) die "missing argument to $1 (try -h)" ;;
196 --program-prefix=*) program_prefix=${1##*=} ;;
197
198 --name) die "missing argument to $1 (try -h)" ;;
199 --name=*) build_dir=${1##*=} ;;
200
201 --cadical) cadical=ON;;
202 --no-cadical) cadical=OFF;;
203
204 --cln) cln=ON;;
205 --no-cln) cln=OFF;;
206
207 --coverage) coverage=ON;;
208 --no-coverage) coverage=OFF;;
209
210 --cryptominisat) cryptominisat=ON;;
211 --no-cryptominisat) cryptominisat=OFF;;
212
213 --debug-symbols) debug_symbols=ON;;
214 --no-debug-symbols) debug_symbols=OFF;;
215
216 --debug-context-mm) debug_context_mm=ON;;
217 --no-debug-context-mm) debug_context_mm=OFF;;
218
219 --dumping) dumping=ON;;
220 --no-dumping) dumping=OFF;;
221
222 --gpl) gpl=ON;;
223 --no-gpl) gpl=OFF;;
224
225 --kissat) kissat=ON;;
226 --no-kissat) kissat=OFF;;
227
228 --win64) win64=ON;;
229
230 --arm64) arm64=ON;;
231
232 --ninja) ninja=ON;;
233
234 --docs) docs=ON;;
235 --no-docs) docs=OFF;;
236
237 --glpk) glpk=ON;;
238 --no-glpk) glpk=OFF;;
239
240 --poly) poly=ON;;
241 --no-poly) poly=OFF;;
242
243 --muzzle) muzzle=ON;;
244 --no-muzzle) muzzle=OFF;;
245
246 --static) shared=OFF; static_binary=ON;;
247 --no-static) shared=ON;;
248
249 --static-binary) static_binary=ON;;
250 --no-static-binary) static_binary=OFF;;
251
252 --auto-download) auto_download=ON;;
253 --no-auto-download) auto_download=OFF;;
254
255 --statistics) statistics=ON;;
256 --no-statistics) statistics=OFF;;
257
258 --symfpu) symfpu=ON;;
259 --no-symfpu) symfpu=OFF;;
260
261 --tracing) tracing=ON;;
262 --no-tracing) tracing=OFF;;
263
264 --unit-testing) unit_testing=ON;;
265 --no-unit-testing) unit_testing=OFF;;
266
267 --python2) python2=ON;;
268 --no-python2) python2=OFF;;
269
270 --python-bindings) python_bindings=ON;;
271 --no-python-bindings) python_bindings=OFF;;
272
273 --java-bindings) java_bindings=ON;;
274 --no-java-bindings) java_bindings=OFF;;
275
276 --all-bindings)
277 python_bindings=ON
278 java_bindings=ON;;
279
280 --valgrind) valgrind=ON;;
281 --no-valgrind) valgrind=OFF;;
282
283 --profiling) profiling=ON;;
284 --no-profiling) profiling=OFF;;
285
286 --editline) editline=ON;;
287 --no-editline) editline=OFF;;
288
289 --abc-dir) die "missing argument to $1 (try -h)" ;;
290 --abc-dir=*) abc_dir=${1##*=} ;;
291
292 --glpk-dir) die "missing argument to $1 (try -h)" ;;
293 --glpk-dir=*) glpk_dir=${1##*=} ;;
294
295 --dep-path) die "missing argument to $1 (try -h)" ;;
296 --dep-path=*) dep_path="${dep_path};${1##*=}" ;;
297
298 --lib-only) lib_only=ON ;;
299
300 -*) die "invalid option '$1' (try -h)";;
301
302 *) case $1 in
303 production) buildtype=Production;;
304 debug) buildtype=Debug;;
305 testing) buildtype=Testing;;
306 competition) buildtype=Competition;;
307 competition-inc) buildtype=Competition; comp_inc=ON;;
308 *) die "invalid build type (try -h)";;
309 esac
310 ;;
311 esac
312 shift
313 done
314
315 #--------------------------------------------------------------------------#
316
317 if [ $werror != default ]; then
318 export CFLAGS=-Werror
319 export CXXFLAGS=-Werror
320 fi
321
322 cmake_opts=""
323
324 [ $buildtype != default ] \
325 && cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype"
326
327 [ $asan != default ] \
328 && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan"
329 [ $auto_download != default ] \
330 && cmake_opts="$cmake_opts -DENABLE_AUTO_DOWNLOAD=$auto_download"
331 [ $ubsan != default ] \
332 && cmake_opts="$cmake_opts -DENABLE_UBSAN=$ubsan"
333 [ $tsan != default ] \
334 && cmake_opts="$cmake_opts -DENABLE_TSAN=$tsan"
335 [ $assertions != default ] \
336 && cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions"
337 [ $comp_inc != default ] \
338 && cmake_opts="$cmake_opts -DENABLE_COMP_INC_TRACK=$comp_inc"
339 [ $coverage != default ] \
340 && cmake_opts="$cmake_opts -DENABLE_COVERAGE=$coverage"
341 [ $debug_symbols != default ] \
342 && cmake_opts="$cmake_opts -DENABLE_DEBUG_SYMBOLS=$debug_symbols"
343 [ $debug_context_mm != default ] \
344 && cmake_opts="$cmake_opts -DENABLE_DEBUG_CONTEXT_MM=$debug_context_mm"
345 [ $dumping != default ] \
346 && cmake_opts="$cmake_opts -DENABLE_DUMPING=$dumping"
347 [ $gpl != default ] \
348 && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl"
349 [ $win64 != default ] \
350 && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake"
351 [ $arm64 != default ] \
352 && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-aarch64.cmake"
353 [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
354 [ $muzzle != default ] \
355 && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
356 [ $shared != default ] \
357 && cmake_opts="$cmake_opts -DENABLE_SHARED=$shared"
358 [ $static_binary != default ] \
359 && cmake_opts="$cmake_opts -DENABLE_STATIC_BINARY=$static_binary"
360 [ $statistics != default ] \
361 && cmake_opts="$cmake_opts -DENABLE_STATISTICS=$statistics"
362 [ $tracing != default ] \
363 && cmake_opts="$cmake_opts -DENABLE_TRACING=$tracing"
364 [ $unit_testing != default ] \
365 && cmake_opts="$cmake_opts -DENABLE_UNIT_TESTING=$unit_testing"
366 [ $python2 != default ] \
367 && cmake_opts="$cmake_opts -DUSE_PYTHON2=$python2"
368 [ $docs != default ] \
369 && cmake_opts="$cmake_opts -DBUILD_DOCS=$docs"
370 [ $python_bindings != default ] \
371 && cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$python_bindings"
372 [ $java_bindings != default ] \
373 && cmake_opts="$cmake_opts -DBUILD_BINDINGS_JAVA=$java_bindings"
374 [ $valgrind != default ] \
375 && cmake_opts="$cmake_opts -DENABLE_VALGRIND=$valgrind"
376 [ $profiling != default ] \
377 && cmake_opts="$cmake_opts -DENABLE_PROFILING=$profiling"
378 [ $editline != default ] \
379 && cmake_opts="$cmake_opts -DUSE_EDITLINE=$editline"
380 [ $abc != default ] \
381 && cmake_opts="$cmake_opts -DUSE_ABC=$abc"
382 [ $cadical != default ] \
383 && cmake_opts="$cmake_opts -DUSE_CADICAL=$cadical"
384 [ $cln != default ] \
385 && cmake_opts="$cmake_opts -DUSE_CLN=$cln"
386 [ $cryptominisat != default ] \
387 && cmake_opts="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat"
388 [ $glpk != default ] \
389 && cmake_opts="$cmake_opts -DUSE_GLPK=$glpk"
390 [ $kissat != default ] \
391 && cmake_opts="$cmake_opts -DUSE_KISSAT=$kissat"
392 [ $poly != default ] \
393 && cmake_opts="$cmake_opts -DUSE_POLY=$poly"
394 [ $symfpu != default ] \
395 && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu"
396 [ "$abc_dir" != default ] \
397 && cmake_opts="$cmake_opts -DABC_DIR=$abc_dir"
398 [ "$glpk_dir" != default ] \
399 && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir"
400 [ "$dep_path" != default ] \
401 && cmake_opts="$cmake_opts -DCMAKE_PREFIX_PATH=$dep_path"
402 [ "$lib_only" != default ] \
403 && cmake_opts="$cmake_opts -DBUILD_LIB_ONLY=$lib_only"
404 [ "$install_prefix" != default ] \
405 && cmake_opts="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix"
406 [ -n "$program_prefix" ] \
407 && cmake_opts="$cmake_opts -DPROGRAM_PREFIX=$program_prefix"
408
409 root_dir=$(pwd)
410
411 # The cmake toolchain can't be changed once it is configured in $build_dir.
412 # Thus, remove $build_dir and create an empty directory.
413 [ $win64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir"
414 [ $arm64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir"
415 mkdir -p "$build_dir"
416
417 cd "$build_dir"
418
419 [ -e CMakeCache.txt ] && rm CMakeCache.txt
420 build_dir_escaped=$(echo "$build_dir" | sed 's/\//\\\//g')
421 cmake "$root_dir" $cmake_opts 2>&1 | \
422 sed "s/^Now just/Now change to '$build_dir_escaped' and/"