configure.ac

   1 #                                               -*- Autoconf -*-
   2 # Process this file with autoconf to produce a configure script.
   3
   4 dnl Preprocess CL args. Defined in config/cvc4.m4
   5 CVC4_AC_INIT
   6
   7 AC_PREREQ(2.61)
   8 AC_INIT
   9 AC_CONFIG_SRCDIR([src/include/cvc4_config.h])
  10 AC_CONFIG_AUX_DIR([config])
  11 AC_CONFIG_MACRO_DIR([config])
  12
  13 m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])])
  14
  15 CVC4_MAJOR=0
  16 CVC4_MINOR=0
  17 CVC4_RELEASE=0
  18 CVC4_RELEASE_STRING=prerelease
  19
  20 # Libtool version numbers for libraries
  21 # Version numbers are in the form current:revision:age
  22 #
  23 # current -
  24 #   increment if interfaces have been added, removed or changed
  25 # revision -
  26 #   increment if source code has changed
  27 #   set to zero if current is incremented
  28 # age -
  29 #   increment if interfaces have been added
  30 #   set to zero if interfaces have been removed
  31 #   or changed
  32 #
  33 # For more information, see:
  34 # http://www.gnu.org/software/libtool/manual/libtool.html#Versioning
  35 # For guidance on when to change the version number, refer to the
  36 # developer's guide.
  37
  38 CVC4_LIBRARY_VERSION=$CVC4_MAJOR:$CVC4_MINOR:$CVC4_RELEASE
  39 CVC4_PARSER_LIBRARY_VERSION=$CVC4_MAJOR:$CVC4_MINOR:$CVC4_RELEASE
  40
  41 # Using the AC_CANONICAL_* macros destroy the command line you get
  42 # from $@, which we want later for determining the build profile.  So
  43 # we save it.  (We can't do our build profile stuff here, or it's not
  44 # included in the output... autoconf overrides us on the orderings of
  45 # some things.)
  46 config_cmdline="$@"
  47
  48 # turn off static lib building by default
  49 AC_ENABLE_SHARED
  50 AC_DISABLE_STATIC
  51
  52 AC_CANONICAL_BUILD
  53 AC_CANONICAL_HOST
  54 AC_CANONICAL_TARGET
  55
  56 # Features requested by the user
  57 AC_MSG_CHECKING([for requested build profile])
  58 AC_ARG_WITH([build],
  59   [AS_HELP_STRING([--with-build=profile],
  60      [for profile in {production,debug,default,competition}])])
  61
  62 if test -z "${with_build+set}" -o "$with_build" = default; then
  63   with_build=default
  64 fi
  65 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
  66   custom_build_profile=no
  67 else
  68   custom_build_profile=yes
  69 fi
  70 btargs=
  71 if test -n "${enable_optimized+set}"; then
  72   if test "$enable_optimized" = yes; then
  73     btargs="$btargs optimized"
  74   else
  75     btargs="$btargs nooptimized"
  76   fi
  77 fi
  78 if test -n "${enable_debug_symbols+set}"; then
  79   if test "$enable_debug_symbols" = yes; then
  80     btargs="$btargs debugsymbols"
  81   else
  82     btargs="$btargs nodebugsymbols"
  83   fi
  84 fi
  85 if test -n "${enable_assertions+set}"; then
  86   if test "$enable_assertions" = yes; then
  87     btargs="$btargs assertions"
  88   else
  89     btargs="$btargs noassertions"
  90   fi
  91 fi
  92 if test -n "${enable_tracing+set}"; then
  93   if test "$enable_tracing" = yes; then
  94     btargs="$btargs tracing"
  95   else
  96     btargs="$btargs notracing"
  97   fi
  98 fi
  99 if test -n "${enable_muzzle+set}"; then
 100   if test "$enable_muzzle" = yes; then
 101     btargs="$btargs muzzle"
 102   else
 103     btargs="$btargs nomuzzle"
 104   fi
 105 fi
 106 if test -n "${enable_coverage+set}"; then
 107   if test "$enable_coverage" = yes; then
 108     btargs="$btargs coverage"
 109   else
 110     btargs="$btargs nocoverage"
 111   fi
 112 fi
 113 if test -n "${enable_profiling+set}"; then
 114   if test "$enable_profiling" = yes; then
 115     btargs="$btargs profiling"
 116   else
 117     btargs="$btargs noprofiling"
 118   fi
 119 fi
 120 AC_MSG_RESULT([$with_build])
 121
 122 AC_MSG_CHECKING([for appropriate build string])
 123 build_type=`$ac_confdir/config/build-type $with_build $btargs`
 124 if test "$custom_build_profile" = yes; then
 125   if test "$with_build" = default; then
 126     build_type=`$ac_confdir/config/build-type custom $btargs`
 127   fi
 128 fi
 129 AC_MSG_RESULT($build_type)
 130
 131 # Require building in target and build-specific build directory:
 132 #
 133 # If the configure script is invoked from the top-level source
 134 # directory, it creates a suitable build directory (based on the build
 135 # architecture and build profile from $build_type), changes into it,
 136 # and reinvokes itself.  CVC4_CONFIGURE_IN_BUILDS is an envariable
 137 # that breaks any possibility of infinite recursion in this process.
 138 AC_MSG_CHECKING([what dir to configure])
 139 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
 140   AC_MSG_RESULT([this one (in builds/)])
 141 elif test -e src/include/cvc4_config.h; then
 142   AC_MSG_RESULT([builds/$target/$build_type])
 143   echo
 144   if test -z "$ac_srcdir"; then
 145     mkbuilddir=./config/mkbuilddir
 146   else
 147     mkbuilddir=$ac_srcdir/config/mkbuilddir
 148   fi
 149   echo $mkbuilddir "$target" "$build_type"
 150   $mkbuilddir "$target" "$build_type"
 151   echo cd "builds/$target/$build_type"
 152   cd "builds/$target/$build_type"
 153   CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
 154   echo ../../../configure $config_cmdline
 155   exec ../../../configure $config_cmdline
 156 else
 157   AC_MSG_RESULT([this one (user-specified)])
 158 fi
 159
 160 # Unpack standard build types. Any particular options can be overriden with
 161 # --enable/disable-X options
 162 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
 163 # our defaults for CXXFLAGS are better than autoconf's
 164 if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi
 165 case "$with_build" in
 166   production) # highly optimized, no assertions, no tracing
 167     CVC4CPPFLAGS=
 168     CVC4CXXFLAGS=
 169     CVC4LDFLAGS=
 170     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=3                       ; fi
 171     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 172     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 173     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
 174     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
 175     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 176     ;;
 177   debug) # unoptimized, debug symbols, assertions, tracing
 178     CVC4CPPFLAGS=-DCVC4_DEBUG
 179     CVC4CXXFLAGS='-fno-inline'
 180     CVC4LDFLAGS=
 181     if test -z "${enable_optimized+set}"    ; then enable_optimized=no              ; fi
 182     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 183     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
 184     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
 185     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 186     ;;
 187   default) # moderately optimized, assertions, tracing
 188     CVC4CPPFLAGS=
 189     CVC4CXXFLAGS=
 190     CVC4LDFLAGS=
 191     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=2                       ; fi
 192     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 193     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 194     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
 195     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
 196     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 197     ;;
 198   competition) # maximally optimized, no assertions, no tracing, muzzled
 199     CVC4CPPFLAGS=
 200     CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
 201     CVC4LDFLAGS=
 202     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=9                       ; fi
 203     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 204     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no          ; fi
 205     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
 206     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
 207     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=yes                ; fi
 208     ;;
 209   *)
 210     AC_MSG_FAILURE([unknown build profile: $with_build])
 211     ;;
 212 esac
 213
 214 # permit a static binary
 215 AC_MSG_CHECKING([whether to build a static binary])
 216 AC_ARG_ENABLE([static-binary],
 217      [AS_HELP_STRING([--enable-static-binary],
 218                      [build a statically-linked binary [default=no]])])
 219 if test -z "${enable_static_binary+set}"; then
 220   enable_static_binary=no
 221 fi
 222 AC_MSG_RESULT([$enable_static_binary])
 223 if test "${enable_static_binary}" = yes -a "${enable_static}" != yes; then
 224   enable_static=yes
 225   AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
 226 fi
 227
 228 AC_MSG_CHECKING([whether to optimize libcvc4])
 229
 230 AC_ARG_ENABLE([optimized],
 231   [AS_HELP_STRING([--enable-optimized],
 232      [optimize the build])])
 233
 234 if test -z "${enable_optimized+set}"; then
 235   enable_optimized=no
 236 fi
 237
 238 AC_MSG_RESULT([$enable_optimized])
 239
 240 if test "$enable_optimized" = yes; then
 241   CVC4CXXFLAGS="$CVC4CXXFLAGS -O$OPTLEVEL"
 242 else
 243   CVC4CXXFLAGS="$CVC4CXXFLAGS -O0"
 244 fi
 245
 246 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
 247
 248 AC_ARG_ENABLE([debug-symbols],
 249   [AS_HELP_STRING([--disable-debug-symbols],
 250      [do not include debug symbols in libcvc4])])
 251
 252 if test -z "${enable_debug_symbols+set}"; then
 253   enable_debug_symbols=yes
 254 fi
 255
 256 AC_MSG_RESULT([$enable_debug_symbols])
 257
 258 if test "$enable_debug_symbols" = yes; then
 259   CVC4CXXFLAGS="$CVC4CXXFLAGS -ggdb3"
 260 fi
 261
 262 AC_MSG_CHECKING([whether to include assertions in build])
 263
 264 AC_ARG_ENABLE([assertions],
 265   [AS_HELP_STRING([--disable-assertions],
 266      [turn off assertions in build])])
 267
 268 if test -z "${enable_assertions+set}"; then
 269   enable_assertions=yes
 270 fi
 271
 272 AC_MSG_RESULT([$enable_assertions])
 273
 274 if test "$enable_assertions" = yes; then
 275   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_ASSERTIONS"
 276 fi
 277
 278 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
 279 AC_ARG_ENABLE([tracing],
 280   [AS_HELP_STRING([--disable-tracing],
 281      [remove all tracing code from CVC4])])
 282
 283 if test -z "${enable_tracing+set}"; then
 284   enable_tracing=yes
 285 fi
 286
 287 AC_MSG_RESULT([$enable_tracing])
 288
 289 if test "$enable_tracing" = yes; then
 290   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_TRACING"
 291 fi
 292
 293 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
 294 AC_ARG_ENABLE([muzzle],
 295   [AS_HELP_STRING([--enable-muzzle],
 296      [completely silence CVC4; remove ALL non-result output from build])])
 297
 298 if test -z "${enable_muzzle+set}"; then
 299   enable_muzzle=no
 300 fi
 301
 302 AC_MSG_RESULT([$enable_muzzle])
 303
 304 if test "$enable_muzzle" = yes; then
 305   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_MUZZLE"
 306 fi
 307
 308 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
 309 AC_ARG_ENABLE([coverage],
 310   [AS_HELP_STRING([--enable-coverage],
 311      [build with support for gcov coverage testing])])
 312
 313 if test -z "${enable_coverage+set}"; then
 314   enable_coverage=no
 315 fi
 316
 317 AC_MSG_RESULT([$enable_coverage])
 318
 319 if test "$enable_coverage" = yes; then
 320   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_COVERAGE"
 321   CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage"
 322   CVC4LDFLAGS="$CVC4LDFLAGS --coverage"
 323 fi
 324
 325 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
 326
 327 AC_ARG_ENABLE([profiling],
 328   [AS_HELP_STRING([--enable-profiling],
 329      [build with support for gprof profiling])])
 330
 331 if test -z "${enable_profiling+set}"; then
 332   enable_profiling=no
 333 fi
 334
 335 AC_MSG_RESULT([$enable_profiling])
 336
 337 if test "$enable_profiling" = yes; then
 338   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_PROFILING"
 339   CVC4CXXFLAGS="$CVC4CXXFLAGS -pg"
 340   CVC4LDFLAGS="$CVC4LDFLAGS -pg"
 341 fi
 342
 343 AM_INIT_AUTOMAKE(cvc4, $CVC4_RELEASE_STRING)
 344 AC_CONFIG_HEADERS([config.h])
 345
 346 # Initialize libtool's configuration options.
 347 _LT_SET_OPTION([LT_INIT],[win32-dll])
 348 LT_INIT
 349
 350 # Checks for programs.
 351 AC_PROG_CC
 352 AC_PROG_CXX
 353 AC_PROG_INSTALL
 354 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 355 AC_PROG_ANTLR
 356
 357 DX_PDF_FEATURE(OFF)
 358 DX_PS_FEATURE(OFF)
 359 DX_DOT_FEATURE(OFF)
 360 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc)
 361
 362 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
 363
 364 AC_SUBST([CXXTEST])
 365
 366 AC_ARG_WITH([cxxtest-dir],
 367   [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
 368   [CXXTEST="$withval"])
 369
 370 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
 371 # relative path) and having switched the configure directory (see above),
 372 # search with respect to the top source dir, not the build dir
 373 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
 374   case "$CXXTEST" in
 375     /*) ;;
 376     *)  CXXTEST="$srcdir/$CXXTEST" ;;
 377   esac
 378 fi
 379
 380 CXXTESTGEN=
 381 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
 382 if test -z "$CXXTESTGEN"; then
 383   AC_MSG_NOTICE([unit tests disabled, cxxtestgen.pl not found.])
 384 elif test -z "$CXXTEST"; then
 385   CXXTEST=$(dirname "$CXXTESTGEN")
 386   AC_MSG_CHECKING([for location of CxxTest headers])
 387   if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
 388     AC_MSG_RESULT([$CXXTEST])
 389   else
 390     AC_MSG_RESULT([not found])
 391     AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
 392     CXXTESTGEN=
 393     CXXTEST=
 394   fi
 395 fi
 396
 397 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
 398
 399 AC_ARG_VAR(TEST_CPPFLAGS, [CXXFLAGS to use when testing (default=$CPPFLAGS)])
 400 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
 401 AC_ARG_VAR(TEST_LDFLAGS,  [LDFLAGS to use when testing (default=$LDFLAGS)])
 402
 403 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
 404
 405 if test -n "$CXXTEST"; then
 406   if test -z "$PERL"; then
 407     AC_CHECK_PROGS(PERL, perl, perl, [])
 408   else
 409     AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
 410   fi
 411
 412   if test -z "$PERL"; then
 413     AC_MSG_WARN([unit tests disabled, perl not found.])
 414     CXXTESTGEN=
 415     CXXTEST=
 416   fi
 417 fi
 418
 419 # Checks for libraries.
 420 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
 421 AC_CHECK_LIB(gmpxx, __gmpz_init, , [AC_MSG_ERROR([GNU MP C++ library (libgmpxx) not found, see http://gmplib.org/])])
 422
 423 # Check for antlr C++ runtime (defined in config/antlr.m4)
 424 AC_LIB_ANTLR
 425
 426 # Checks for header files.
 427 AC_CHECK_HEADERS([getopt.h unistd.h])
 428
 429 # Checks for typedefs, structures, and compiler characteristics.
 430 #AC_HEADER_STDBOOL
 431 AC_TYPE_UINT16_T
 432 AC_TYPE_UINT32_T
 433 AC_TYPE_UINT64_T
 434 AC_TYPE_SIZE_T
 435
 436 # Checks for library functions.
 437 # (empty)
 438
 439 # Some definitions for config.h
 440 # (empty)
 441
 442 # Prepare configure output
 443
 444 if test "$enable_shared" = yes; then BUILDING_SHARED=1; fi
 445 if test "$enable_static" = yes; then BUILDING_STATIC=1; fi
 446 AC_SUBST(BUILDING_SHARED)
 447 AC_SUBST(BUILDING_STATIC)
 448 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
 449
 450 AC_SUBST(CVC4_LIBRARY_VERSION)
 451 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
 452
 453 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
 454 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
 455 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
 456 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
 457
 458 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS"
 459 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
 460 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 461
 462 # mk_include
 463 #
 464 # When automake scans Makefiles, it complains about non-standard make
 465 # features (including GNU extensions), and breaks GNU Make's
 466 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
 467 # constructs.  automake even follows "include" and messes with
 468 # included Makefiles.
 469 #
 470 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
 471 # have to hide some included Makefiles with GNU extensions.  We do
 472 # this by defining mk_include as an autoconf substitution and then
 473 # using "@mk_include@ other_makefile" in Makefile.am to include
 474 # makefiles with GNU extensions; this hides them from automake.
 475 mk_include=include
 476 AC_SUBST(mk_include)
 477
 478 # CVC4_FALSE
 479 #
 480 # This is used to _always_ comment out rules in automake makefiles, but
 481 # still trigger certain automake behavior; see test/unit/Makefile.am.
 482 AM_CONDITIONAL([CVC4_FALSE], [false])
 483
 484 AC_CONFIG_FILES([
 485   Makefile.builds
 486   Makefile]
 487   m4_esyscmd([find contrib/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,'])
 488 )
 489
 490 AC_OUTPUT
 491
 492 # Final information to the user
 493
 494 if test "$custom_build_profile" = yes; then
 495   if test "$with_build" = default; then
 496     with_build=custom
 497   else
 498     AC_MSG_WARN([])
 499     AC_MSG_WARN([This is a customized $with_build build profile.])
 500     AC_MSG_WARN([])
 501     with_build="$with_build-custom"
 502   fi
 503 fi
 504
 505 support_unit_tests='cxxtest not found; unit tests not supported'
 506 if test -n "$CXXTEST"; then
 507   support_unit_tests='unit testing infrastructure enabled in build directory'
 508 fi
 509
 510 if test "$enable_optimized" = yes; then
 511   optimized="yes, at level $OPTLEVEL"
 512 else
 513   optimized="no"
 514 fi
 515
 516 cat <<EOF
 517
 518 CVC4 $VERSION
 519
 520 Build profile: $with_build
 521 Build ID     : $build_type
 522 Optimized    : $optimized
 523 Debug symbols: $enable_debug_symbols
 524 Assertions   : $enable_assertions
 525 Tracing      : $enable_tracing
 526 Muzzle       : $enable_muzzle
 527 gcov support : $enable_coverage
 528 gprof support: $enable_profiling
 529 unit tests   : $support_unit_tests
 530
 531 static libs  : $enable_static
 532 shared libs  : $enable_shared
 533 static binary: $enable_static_binary
 534
 535 CPPFLAGS     : $CPPFLAGS
 536 CXXFLAGS     : $CXXFLAGS
 537 LDFLAGS      : $LDFLAGS
 538
 539 libcvc4 version      : $CVC4_LIBRARY_VERSION
 540 libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION
 541
 542 Now just type make, followed by make check or make install, as you like.
 543
 544 EOF