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