squash-merge from proof branch

[cvc5.git] / configure.ac

diff --git a/configure.ac b/configure.ac
index 672b70d6df257af3114be8a79aac2a02462928e9..c3c29db38052bab54fae8bbbf0f8fac3059da1bd 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -309,7 +309,9 @@ if test $cvc4_use_cln != 0; then
   PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
     [AC_LANG_PUSH([C++])
      save_LIBS="$LIBS"
+     save_CXXFLAGS="$CXXFLAGS"
      LIBS="$CLN_LIBS $LIBS"
+     CXXFLAGS="$CLN_CFLAGS $CXXFLAGS"
      AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])], [
        cvc4_use_cln=1
      ], [
@@ -323,6 +325,7 @@ if test $cvc4_use_cln != 0; then
          cvc4_use_gmp=1
        fi
      ])
+     CXXFLAGS="$save_CXXFLAGS"
      LIBS="$save_LIBS"
      AC_LANG_POP([C++])
     ],
@@ -391,8 +394,10 @@ elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
   $as_echo "cd builds/$target/$build_type"
   cd "builds/$target/$build_type"
   CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
+  # Runs the single recursive configure invocation using a relative path.
+  # See https://lists.gnu.org/archive/html/autoconf/2011-04/msg00060.html
   echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
-  "$SHELL" "`pwd`/../../../configure" "${config_cmdline[[@]]}"
+  "$SHELL" "../../../configure" "${config_cmdline[[@]]}"
   exitval=$?
   cd ../../..
   if test $exitval -eq 0; then
@@ -426,12 +431,13 @@ as_me=configure
 
 # Unpack standard build types. Any particular options can be overriden with
 # --enable/disable-X options
+# Tim: This needs to keep CVC4CPPFLAGS, CVC4CXXFLAGS, etc. set by earlier checks
 case "$with_build" in
   production) # highly optimized, no assertions, no tracing, dumping
-    CVC4CPPFLAGS=
-    CVC4CXXFLAGS=
-    CVC4CFLAGS=
-    CVC4LDFLAGS=
+    CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
+    CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
+    CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
+    CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=3                       ; fi
     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
@@ -439,32 +445,32 @@ case "$with_build" in
     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
     if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
-    if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
+    if test -z "${enable_proof+set}"        ; then enable_proof=yes                 ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     ;;
   debug) # unoptimized, debug symbols, assertions, tracing, dumping
-    CVC4CPPFLAGS='-DCVC4_DEBUG'
-    CVC4CXXFLAGS='-fno-inline'
-    CVC4CFLAGS='-fno-inline'
-    CVC4LDFLAGS=
+    CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG"
+    CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-fno-inline"
+    CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-fno-inline"
+    CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
     FLAG_VISIBILITY_HIDDEN=
     if test -z "${enable_optimized+set}"    ; then enable_optimized=no              ; fi
     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
-    if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
+    if test -z "${enable_proof+set}"        ; then enable_proof=yes                 ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     ;;
   default) # moderately optimized, assertions, tracing, dumping
-    CVC4CPPFLAGS=
-    CVC4CXXFLAGS=
-    CVC4CFLAGS=
-    CVC4LDFLAGS=
+    CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
+    CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
+    CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
+    CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=2                       ; fi
     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
@@ -472,16 +478,16 @@ case "$with_build" in
     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
-    if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
+    if test -z "${enable_proof+set}"        ; then enable_proof=yes                 ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     ;;
   competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
-    CVC4CPPFLAGS='-DCVC4_COMPETITION_MODE'
-    CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
-    CVC4CFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
-    CVC4LDFLAGS=
+    CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COMPETITION_MODE"
+    CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
+    CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
+    CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=9                       ; fi
     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
@@ -535,10 +541,10 @@ fi
 AC_MSG_CHECKING([whether to support proofs in libcvc4])
 
 AC_ARG_ENABLE([proof],
-  [AS_HELP_STRING([--enable-proof],
-     [support proof generation])])
+  [AS_HELP_STRING([--disable-proof],
+     [do not support proof generation])])
 if test -z "${enable_proof+set}"; then
-  enable_proof=no
+  enable_proof=yes
 fi
 AC_MSG_RESULT([$enable_proof])
 
@@ -1404,9 +1410,9 @@ if test -n "$CVC4_LANGUAGE_BINDINGS"; then
   fi
 fi
 
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/base/tls.h])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
 
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])