diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-18 22:02:11 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-18 22:02:11 +0000 |
commit | 394791604a62e19763a8a45328bc5177d91fabf9 (patch) | |
tree | 29027c84c0285da33bac6c5d1366635b9e4db1bc /configure.ac | |
parent | 477e97cd81afe4b86eea47e9abe6311fc22299fc (diff) |
work on exprs, driver, util
Diffstat (limited to 'configure.ac')
-rw-r--r-- | configure.ac | 56 |
1 files changed, 53 insertions, 3 deletions
diff --git a/configure.ac b/configure.ac index 58fcdfac3..77c03ef2c 100644 --- a/configure.ac +++ b/configure.ac @@ -12,6 +12,25 @@ LT_INIT AC_LIBTOOL_WIN32_DLL +# Features requested by the user +AC_MSG_CHECKING([whether to do a debug build of CVC4]) +AC_ARG_ENABLE([debug], [AS_HELP_STRING([--enable-debug] ,[do a debug build of CVC4])]) +if test -z "${enable_debug+set}"; then + enable_debug=no +fi +AC_MSG_RESULT([$enable_debug]) + +AC_MSG_CHECKING([whether to include assertions in build]) +AC_ARG_ENABLE([assertions], [AS_HELP_STRING([--disable-assertions],[turn off assertions in build])]) +if test -z "${enable_assertions+set}"; then + enable_assertions=yes +fi +AC_MSG_RESULT([$enable_assertions]) + +if test "$enable_assertions" = no -a "$enable_debug" = yes; then + AC_MSG_FAILURE([when debugging is on, so must assertions be.]) +fi + # Checks for programs. AC_PROG_CC AC_PROG_CXX @@ -20,15 +39,16 @@ AC_PROG_LIBTOOL AM_PROG_LEX AC_PROG_YACC -AC_CHECK_PROG(DOXYGEN, doxygen, doxygen,) -if test "$DOXYGEN" = ''; then - echo 'WARNING: documentation targets require doxygen. Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.' +AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, []) +if test -z "$DOXYGEN"; then + AC_MSG_WARN([documentation targets require doxygen. Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.]) fi # Checks for libraries. AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])]) # Checks for header files. +AC_CHECK_HEADERS([getopt.h unistd.h]) # Checks for typedefs, structures, and compiler characteristics. AC_HEADER_STDBOOL @@ -39,6 +59,17 @@ AC_TYPE_SIZE_T # Checks for library functions. +# Some definitions for config.h +if test "$enable_debug" = yes; then + AC_DEFINE([CVC4_DEBUG], [], [Whether or not to include debugging code.]) +fi + +if test "$enable_assertions" = yes; then + AC_DEFINE([CVC4_ASSERTIONS], [], [Whether or not assertions are enabled.]) +fi + +# Prepare configure output + AC_CONFIG_FILES([ Makefile contrib/Makefile @@ -54,4 +85,23 @@ AC_CONFIG_FILES([ src/parser/Makefile src/theory/Makefile ]) + AC_OUTPUT + +# Final information to the user +debug=debug +if test "$enable_debug" = no; then + debug=non-debug +fi +withassertions=with +if test "$enable_assertions" = no; then + withassertions=without +fi + +cat <<EOF + +CVC4 $VERSION will be built as a $debug build $withassertions assertions. + +Now just type make, followed by make check or make install, as you like. + +EOF |