configure.ac

   1 #                                               -*- Autoconf -*-
   2 # Process this file with autoconf to produce a configure script.
   3
   4 CVC4_AC_INIT
   5
   6 AC_PREREQ(2.64)
   7 AC_INIT
   8 AC_CONFIG_SRCDIR([src/include/cvc4_config.h])
   9 AC_CONFIG_AUX_DIR([config])
  10 AC_CONFIG_MACRO_DIR([config])
  11
  12 CVC4_RELEASE=prerelease
  13 CVC4_LIBRARY_RELEASE_CODE=0:0:0
  14 CVC4_LIBRARY_VERSION=0:0:0
  15 CVC4_PARSER_LIBRARY_VERSION=0:0:0
  16
  17 # really irritating: AC_CANONICAL_* bash $@
  18 config_cmdline="$@"
  19
  20 # turn off static lib building by default
  21 AC_ENABLE_SHARED
  22 AC_DISABLE_STATIC
  23
  24 AC_CANONICAL_BUILD
  25 AC_CANONICAL_HOST
  26 AC_CANONICAL_TARGET
  27
  28 # Features requested by the user
  29 AC_MSG_CHECKING([for requested build profile])
  30 AC_ARG_WITH([build],             [AS_HELP_STRING([--with-build=profile],     [for profile in {production,debug,default,competition}])])
  31 if test -z "${with_build+set}" -o "$with_build" = default; then
  32   with_build=default
  33 fi
  34 if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}"; then
  35   non_standard_build_profile=no
  36 else
  37   non_standard_build_profile=yes
  38 fi
  39 build_type_suffix=
  40 if test -n "${enable_optimized+set}"; then
  41   if test "$enable_optimized" = no; then
  42     build_type_suffix=$build_type_suffix-noopt
  43   else
  44     build_type_suffix=$build_type_suffix-opt
  45   fi
  46 fi
  47 if test -n "${enable_debug_symbols+set}"; then
  48   if test "$enable_debug_symbols" = no; then
  49     build_type_suffix=$build_type_suffix-nodsy
  50   else
  51     build_type_suffix=$build_type_suffix-dsy
  52   fi
  53 fi
  54 if test -n "${enable_assertions+set}"; then
  55   if test "$enable_assertions" = no; then
  56     build_type_suffix=$build_type_suffix-noass
  57   else
  58     build_type_suffix=$build_type_suffix-ass
  59   fi
  60 fi
  61 if test -n "${enable_tracing+set}"; then
  62   if test "$enable_tracing" = no; then
  63     build_type_suffix=$build_type_suffix-notrc
  64   else
  65     build_type_suffix=$build_type_suffix-trc
  66   fi
  67 fi
  68 if test -n "${enable_muzzle+set}"; then
  69   if test "$enable_muzzle" = no; then
  70     build_type_suffix=$build_type_suffix-nomzl
  71   else
  72     build_type_suffix=$build_type_suffix-mzl
  73   fi
  74 fi
  75 if test -n "${enable_coverage+set}"; then
  76   if test "$enable_coverage" = no; then
  77     build_type_suffix=$build_type_suffix-nocvg
  78   else
  79     build_type_suffix=$build_type_suffix-cvg
  80   fi
  81 fi
  82 if test -n "${enable_profiling+set}"; then
  83   if test "$enable_profiling" = no; then
  84     build_type_suffix=$build_type_suffix-noprf
  85   else
  86     build_type_suffix=$build_type_suffix-prf
  87   fi
  88 fi
  89 AC_MSG_RESULT([$with_build])
  90
  91 AC_MSG_CHECKING([for appropriate build string])
  92 build_type=$with_build$build_type_suffix
  93 if test "$non_standard_build_profile" = yes; then
  94   if test "$with_build" = default; then
  95     build_type=custom$build_type_suffix
  96   fi
  97 fi
  98 AC_MSG_RESULT($build_type)
  99
 100 # require building in target and build-specific build directory
 101 AC_MSG_CHECKING([what dir to configure])
 102 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
 103   AC_MSG_RESULT([this one (in builds/)])
 104 elif test -e src/include/cvc4_config.h; then
 105   AC_MSG_RESULT([builds/$target/$build_type])
 106   echo
 107   echo Setting up "builds/$target/$build_type"...
 108   rm -fv config.log config.status confdefs.h
 109   mkdir -pv "builds/$target/$build_type"
 110   ln -sfv "$target/$build_type/Makefile.builds" builds/Makefile
 111   echo Creating builds/current...
 112   (echo "# This is the most-recently-configured CVC4 build"; \
 113    echo "# 'make' in the top-level source directory applies to this build"; \
 114    echo "CURRENT_BUILD = $target/$build_type") > builds/current
 115   echo Linking builds/src...
 116   rm -f builds/src
 117   ln -sfv "$target/$build_type/src" builds/src
 118   echo Linking builds/test...
 119   rm -f builds/test
 120   ln -sfv "$target/$build_type/test" builds/test
 121   echo cd "builds/$target/$build_type"
 122   cd "builds/$target/$build_type"
 123   CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
 124   echo ../../../configure $config_cmdline
 125   exec ../../../configure $config_cmdline
 126 else
 127   AC_MSG_RESULT([this one (user-specified)])
 128 fi
 129
 130 case "$with_build" in
 131   production)
 132     CVC4CPPFLAGS=
 133     CVC4CXXFLAGS=-O3
 134     CVC4LDFLAGS=
 135     if test -z "${enable_assertions+set}"; then enable_assertions=no             ; fi
 136     if test -z "${enable_tracing+set}"   ; then enable_tracing=no                ; fi
 137     if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
 138     ;;
 139   debug)
 140     CVC4CPPFLAGS=-DCVC4_DEBUG
 141     CVC4CXXFLAGS='-O0 -fno-inline -ggdb3'
 142     CVC4LDFLAGS=
 143     if test -z "${enable_assertions+set}"; then enable_assertions=yes            ; fi
 144     if test -z "${enable_tracing+set}"   ; then enable_tracing=yes               ; fi
 145     if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
 146     ;;
 147   default)
 148     CVC4CPPFLAGS=
 149     CVC4CXXFLAGS=-O2
 150     CVC4LDFLAGS=
 151     if test -z "${enable_assertions+set}"; then enable_assertions=yes            ; fi
 152     if test -z "${enable_tracing+set}"   ; then enable_tracing=yes               ; fi
 153     if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
 154     ;;
 155   competition)
 156     CVC4CPPFLAGS=
 157     CVC4CXXFLAGS='-O9 -funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
 158     CVC4LDFLAGS=
 159     if test -z "${enable_assertions+set}"; then enable_assertions=no             ; fi
 160     if test -z "${enable_tracing+set}"   ; then enable_tracing=no                ; fi
 161     if test -z "${enable_muzzle+set}"    ; then enable_muzzle=yes                ; fi
 162     ;;
 163   *)
 164     AC_MSG_FAILURE([unknown build profile: $with_build])
 165     ;;
 166 esac
 167
 168 AC_MSG_CHECKING([whether to optimize libcvc4])
 169 AC_ARG_ENABLE([optimized],       [AS_HELP_STRING([--enable-optimized],       [optimize the build])])
 170 if test -z "${enable_optimized+set}"; then
 171   enable_optimized=no
 172 fi
 173 AC_MSG_RESULT([$enable_optimized])
 174 if test "$enable_optimized" = yes; then
 175   CVC4CXXFLAGS="$CVC4CXXFLAGS -O3"
 176 fi
 177
 178 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
 179 AC_ARG_ENABLE([debug-symbols],   [AS_HELP_STRING([--disable-debug-symbols],  [do not include debug symbols in libcvc4])])
 180 if test -z "${enable_debug_symbols+set}"; then
 181   enable_debug_symbols=yes
 182 fi
 183 AC_MSG_RESULT([$enable_debug_symbols])
 184 if test "$enable_debug_symbols" = yes; then
 185   CVC4CXXFLAGS="$CVC4CXXFLAGS -ggdb3"
 186 fi
 187
 188 AC_MSG_CHECKING([whether to include assertions in build])
 189 AC_ARG_ENABLE([assertions],      [AS_HELP_STRING([--disable-assertions],     [turn off assertions in build])])
 190 if test -z "${enable_assertions+set}"; then
 191   enable_assertions=yes
 192 fi
 193 AC_MSG_RESULT([$enable_assertions])
 194 if test "$enable_assertions" = yes; then
 195   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_ASSERTIONS"
 196 fi
 197
 198 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
 199 AC_ARG_ENABLE([tracing],         [AS_HELP_STRING([--disable-tracing],        [remove all tracing code from CVC4])])
 200 if test -z "${enable_tracing+set}"; then
 201   enable_tracing=yes
 202 fi
 203 AC_MSG_RESULT([$enable_tracing])
 204 if test "$enable_tracing" = yes; then
 205   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_TRACING"
 206 fi
 207
 208 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
 209 AC_ARG_ENABLE([muzzle],          [AS_HELP_STRING([--enable-muzzle],          [completely silence CVC4; remove ALL non-result output from build])])
 210 if test -z "${enable_muzzle+set}"; then
 211   enable_muzzle=no
 212 fi
 213 AC_MSG_RESULT([$enable_muzzle])
 214 if test "$enable_muzzle" = yes; then
 215   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_MUZZLE"
 216 fi
 217
 218 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
 219 AC_ARG_ENABLE([coverage],        [AS_HELP_STRING([--enable-coverage],        [build with support for gcov coverage testing])])
 220 if test -z "${enable_coverage+set}"; then
 221   enable_coverage=no
 222 fi
 223 AC_MSG_RESULT([$enable_coverage])
 224 if test "$enable_coverage" = yes; then
 225   CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage"
 226   CVC4LDFLAGS="$CVC4LDFLAGS --coverage"
 227 fi
 228
 229 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
 230 AC_ARG_ENABLE([profiling],       [AS_HELP_STRING([--enable-profiling],       [build with support for gprof profiling])])
 231 if test -z "${enable_profiling+set}"; then
 232   enable_profiling=no
 233 fi
 234 AC_MSG_RESULT([$enable_profiling])
 235 if test "$enable_profiling" = yes; then
 236   CVC4CXXFLAGS="$CVC4CXXFLAGS -pg"
 237   CVC4LDFLAGS="$CVC4LDFLAGS -pg"
 238 fi
 239
 240 AM_INIT_AUTOMAKE(cvc4, $CVC4_RELEASE)
 241 AC_CONFIG_HEADERS([config.h])
 242
 243 # keep track of whether the user set these (check here, because
 244 # autoconf might set a default later)
 245 AC_MSG_CHECKING([for user CPPFLAGS])
 246 if test -z "${CPPFLAGS+set}"; then user_cppflags=no; else user_cppflags=yes; fi
 247 AC_MSG_RESULT([${CPPFLAGS-none}])
 248 AC_MSG_CHECKING([for user CXXFLAGS])
 249 if test -z "${CXXFLAGS+set}"; then user_cxxflags=no; else user_cxxflags=yes; fi
 250 AC_MSG_RESULT([${CXXFLAGS-none}])
 251 AC_MSG_CHECKING([for user LDFLAGS])
 252 if test -z "${LDFLAGS+set}" ; then user_ldflags=no ; else user_ldflags=yes ; fi
 253 AC_MSG_RESULT([${LDFLAGS-none}])
 254
 255 _LT_SET_OPTION([LT_INIT],[win32-dll])
 256 LT_INIT
 257
 258
 259 # Checks for programs.
 260 AC_PROG_CC
 261 AC_PROG_CXX
 262 AC_PROG_INSTALL
 263 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 264 AC_PROG_ANTLR
 265
 266 AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, [])
 267 if test -z "$DOXYGEN"; then
 268   AC_MSG_WARN([documentation targets require doxygen.  Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.])
 269 fi
 270 AC_ARG_VAR(DOXYGEN, [location of doxygen binary])
 271
 272 AC_ARG_VAR(CXXTEST, [path to cxxtest installation])
 273 CXXTESTGEN=
 274 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
 275 if test -z "$CXXTESTGEN"; then
 276   AC_MSG_NOTICE([unit tests disabled, cxxtestgen.pl not found.])
 277 elif test -z "$CXXTEST"; then
 278   CXXTEST=$(dirname "$CXXTESTGEN")
 279   AC_MSG_CHECKING([for location of CxxTest headers])
 280   if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
 281     AC_MSG_RESULT([$CXXTEST])
 282   else
 283     AC_MSG_RESULT([not found])
 284     AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
 285     CXXTESTGEN=
 286     CXXTEST=
 287   fi
 288 fi
 289 AC_ARG_WITH([cxxtest], [AS_HELP_STRING([--with-cxxtest=dir], [path to CxxTest installation])])
 290 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
 291
 292 AC_ARG_VAR(TEST_CPPFLAGS, [CXXFLAGS to use when testing (default=$CPPFLAGS)])
 293 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
 294 AC_ARG_VAR(TEST_LDFLAGS,  [LDFLAGS to use when testing (default=$LDFLAGS)])
 295
 296 if test -n "$CXXTEST"; then
 297   AC_CHECK_PROG(PERL, perl, perl, [])
 298   if test -z "$PERL"; then
 299     AC_MSG_WARN([unit tests disabled, perl not found.])
 300     CXXTESTGEN=
 301     CXXTEST=
 302   fi
 303 fi
 304
 305 # Checks for libraries.
 306 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])])
 307 # Check for antlr C++ runtime (defined in config/antlr.m4)
 308 AC_LIB_ANTLR
 309
 310
 311 # Checks for header files.
 312 AC_CHECK_HEADERS([getopt.h unistd.h])
 313
 314 # Checks for typedefs, structures, and compiler characteristics.
 315 AC_HEADER_STDBOOL
 316 AC_TYPE_UINT16_T
 317 AC_TYPE_UINT32_T
 318 AC_TYPE_UINT64_T
 319 AC_TYPE_SIZE_T
 320
 321 # Checks for library functions.
 322
 323 # Some definitions for config.h
 324
 325 # Prepare configure output
 326
 327 AC_SUBST(CVC4_LIBRARY_RELEASE_CODE)
 328 AC_SUBST(CVC4_LIBRARY_VERSION)
 329 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
 330 if test "$user_cppflags" = no; then
 331   CPPFLAGS="$CVC4CPPFLAGS"
 332 fi
 333 if test "$user_cxxflags" = no; then
 334   CXXFLAGS="$CVC4CXXFLAGS"
 335 fi
 336 if test "$user_ldflags" = no; then
 337   LDFLAGS="$CVC4LDFLAGS"
 338 fi
 339
 340 AC_CONFIG_FILES([
 341   Makefile.builds
 342   Makefile
 343   contrib/Makefile
 344   doc/Makefile
 345   src/Makefile
 346   src/expr/Makefile
 347   src/smt/Makefile
 348   src/main/Makefile
 349   src/prop/minisat/Makefile
 350   src/prop/Makefile
 351   src/util/Makefile
 352   src/context/Makefile
 353   src/parser/Makefile
 354   src/parser/cvc/Makefile
 355   src/parser/smt/Makefile
 356   src/theory/Makefile
 357   src/theory/uf/Makefile
 358   test/Makefile
 359   test/regress/Makefile
 360   test/unit/Makefile
 361 ])
 362
 363 AC_OUTPUT
 364
 365 # Final information to the user
 366
 367 non_standard=
 368 if test "$non_standard_build_profile" = yes; then
 369   if test "$with_build" = default; then
 370     with_build=custom
 371   else
 372     AC_MSG_WARN([])
 373     AC_MSG_WARN([This is a non-standard $with_build build profile.])
 374     AC_MSG_WARN([])
 375     non_standard=-custom
 376   fi
 377 fi
 378
 379 support_unit_tests='cxxtest not found; unit tests not supported'
 380 if test -n "$CXXTEST"; then
 381   support_unit_tests='unit testing infrastructure enabled in build directory'
 382 fi
 383
 384 cat <<EOF
 385
 386 CVC4 $VERSION
 387
 388 Build profile: $with_build$non_standard
 389 Build ID     : $build_type
 390 Optimized    : $enable_optimized
 391 Debug symbols: $enable_debug_symbols
 392 Assertions   : $enable_assertions
 393 Tracing      : $enable_tracing
 394 Muzzle       : $enable_muzzle
 395 gcov support : $enable_coverage
 396 gprof support: $enable_profiling
 397 unit tests   : $support_unit_tests
 398
 399 CPPFLAGS     : $CPPFLAGS
 400 CXXFLAGS     : $CXXFLAGS
 401 LDFLAGS      : $LDFLAGS
 402
 403 Library releases     : $CVC4_LIBRARY_RELEASE_CODE
 404 libcvc4 version      : $CVC4_LIBRARY_VERSION
 405 libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION
 406
 407 Now just type make, followed by make check or make install, as you like.
 408
 409 You can use 'make <build_profile>' to reconfig/build a different profile.
 410 Build profiles: production optimized default competition
 411
 412 EOF
 413
 414 if test "$user_cppflags" = yes; then
 415   AC_MSG_WARN([])
 416   AC_MSG_WARN([I won't override your CPPFLAGS setting.  But some of your build options to configure may not be honored.])
 417   AC_MSG_WARN([To support your options to configure, I would like to set CPPFLAGS to:])
 418   AC_MSG_WARN([    $CVC4CPPFLAGS])
 419   AC_MSG_WARN([])
 420 fi
 421 if test "$user_cxxflags" = yes; then
 422   AC_MSG_WARN([])
 423   AC_MSG_WARN([I won't override your CXXFLAGS setting.  But some of your build options to configure may not be honored.])
 424   AC_MSG_WARN([To support your options to configure, I would like to set CXXFLAGS to:])
 425   AC_MSG_WARN([    $CVC4CXXFLAGS])
 426   AC_MSG_WARN([])
 427 fi
 428 if test "$user_ldflags" = yes; then
 429   AC_MSG_WARN([])
 430   AC_MSG_WARN([I won't override your LDFLAGS setting.  But some of your build options to configure may not be honored.])
 431   AC_MSG_WARN([To support your options to configure, I would like to set LDFLAGS to:])
 432   AC_MSG_WARN([    $CVC4LDFLAGS])
 433   AC_MSG_WARN([])
 434 fi
 435
 436 if test "$non_standard_build_profile" = yes; then
 437   if test "$with_build" = default; then :; else
 438     AC_MSG_WARN([])
 439     AC_MSG_WARN([This is a non-standard $with_build build profile.])
 440     AC_MSG_WARN([])
 441   fi
 442 fi