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.64)
   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 AC_MSG_CHECKING([whether to optimize libcvc4])
 199
 200 AC_ARG_ENABLE([optimized],
 201   [AS_HELP_STRING([--enable-optimized],
 202      [optimize the build])])
 203
 204 if test -z "${enable_optimized+set}"; then
 205   enable_optimized=no
 206 fi
 207
 208 AC_MSG_RESULT([$enable_optimized])
 209
 210 if test "$enable_optimized" = yes; then
 211   CVC4CXXFLAGS="$CVC4CXXFLAGS -O3"
 212 fi
 213
 214 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
 215
 216 AC_ARG_ENABLE([debug-symbols],
 217   [AS_HELP_STRING([--disable-debug-symbols],
 218      [do not include debug symbols in libcvc4])])
 219
 220 if test -z "${enable_debug_symbols+set}"; then
 221   enable_debug_symbols=yes
 222 fi
 223
 224 AC_MSG_RESULT([$enable_debug_symbols])
 225
 226 if test "$enable_debug_symbols" = yes; then
 227   CVC4CXXFLAGS="$CVC4CXXFLAGS -ggdb3"
 228 fi
 229
 230 AC_MSG_CHECKING([whether to include assertions in build])
 231
 232 AC_ARG_ENABLE([assertions],
 233   [AS_HELP_STRING([--disable-assertions],
 234      [turn off assertions in build])])
 235
 236 if test -z "${enable_assertions+set}"; then
 237   enable_assertions=yes
 238 fi
 239
 240 AC_MSG_RESULT([$enable_assertions])
 241
 242 if test "$enable_assertions" = yes; then
 243   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_ASSERTIONS"
 244 fi
 245
 246 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
 247 AC_ARG_ENABLE([tracing],
 248   [AS_HELP_STRING([--disable-tracing],
 249      [remove all tracing code from CVC4])])
 250
 251 if test -z "${enable_tracing+set}"; then
 252   enable_tracing=yes
 253 fi
 254
 255 AC_MSG_RESULT([$enable_tracing])
 256
 257 if test "$enable_tracing" = yes; then
 258   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_TRACING"
 259 fi
 260
 261 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
 262 AC_ARG_ENABLE([muzzle],
 263   [AS_HELP_STRING([--enable-muzzle],
 264      [completely silence CVC4; remove ALL non-result output from build])])
 265
 266 if test -z "${enable_muzzle+set}"; then
 267   enable_muzzle=no
 268 fi
 269
 270 AC_MSG_RESULT([$enable_muzzle])
 271
 272 if test "$enable_muzzle" = yes; then
 273   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_MUZZLE"
 274 fi
 275
 276 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
 277 AC_ARG_ENABLE([coverage],
 278   [AS_HELP_STRING([--enable-coverage],
 279      [build with support for gcov coverage testing])])
 280
 281 if test -z "${enable_coverage+set}"; then
 282   enable_coverage=no
 283 fi
 284
 285 AC_MSG_RESULT([$enable_coverage])
 286
 287 if test "$enable_coverage" = yes; then
 288   CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage"
 289   CVC4LDFLAGS="$CVC4LDFLAGS --coverage"
 290 fi
 291
 292 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
 293
 294 AC_ARG_ENABLE([profiling],
 295   [AS_HELP_STRING([--enable-profiling],
 296      [build with support for gprof profiling])])
 297
 298 if test -z "${enable_profiling+set}"; then
 299   enable_profiling=no
 300 fi
 301
 302 AC_MSG_RESULT([$enable_profiling])
 303
 304 if test "$enable_profiling" = yes; then
 305   CVC4CXXFLAGS="$CVC4CXXFLAGS -pg"
 306   CVC4LDFLAGS="$CVC4LDFLAGS -pg"
 307 fi
 308
 309 AM_INIT_AUTOMAKE(cvc4, $CVC4_RELEASE_STRING)
 310 AC_CONFIG_HEADERS([config.h])
 311
 312 # Initialize libtool's configuration options.
 313 _LT_SET_OPTION([LT_INIT],[win32-dll])
 314 LT_INIT
 315
 316 # Checks for programs.
 317 AC_PROG_CC
 318 AC_PROG_CXX
 319 AC_PROG_INSTALL
 320 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 321 AC_PROG_ANTLR
 322
 323 DX_PDF_FEATURE(OFF)
 324 DX_PS_FEATURE(OFF)
 325 DX_DOT_FEATURE(OFF)
 326 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc)
 327
 328 AC_SUBST([CXXTEST])
 329
 330 AC_ARG_WITH([cxxtest-dir],
 331   [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
 332   [CXXTEST="$withval"])
 333
 334 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
 335 # relative path) and having switched the configure directory (see above),
 336 # search with respect to the top source dir, not the build dir
 337 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
 338   case "$CXXTEST" in
 339     /*) ;;
 340     *)  CXXTEST="$srcdir/$CXXTEST" ;;
 341   esac
 342 fi
 343
 344 CXXTESTGEN=
 345 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
 346 if test -z "$CXXTESTGEN"; then
 347   AC_MSG_NOTICE([unit tests disabled, cxxtestgen.pl not found.])
 348 elif test -z "$CXXTEST"; then
 349   CXXTEST=$(dirname "$CXXTESTGEN")
 350   AC_MSG_CHECKING([for location of CxxTest headers])
 351   if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
 352     AC_MSG_RESULT([$CXXTEST])
 353   else
 354     AC_MSG_RESULT([not found])
 355     AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
 356     CXXTESTGEN=
 357     CXXTEST=
 358   fi
 359 fi
 360
 361 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
 362
 363 AC_ARG_VAR(TEST_CPPFLAGS, [CXXFLAGS to use when testing (default=$CPPFLAGS)])
 364 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
 365 AC_ARG_VAR(TEST_LDFLAGS,  [LDFLAGS to use when testing (default=$LDFLAGS)])
 366
 367 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
 368
 369 if test -n "$CXXTEST"; then
 370   if test -z "$PERL"; then
 371     AC_CHECK_PROGS(PERL, perl, perl, [])
 372   else
 373     AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
 374   fi
 375
 376   if test -z "$PERL"; then
 377     AC_MSG_WARN([unit tests disabled, perl not found.])
 378     CXXTESTGEN=
 379     CXXTEST=
 380   fi
 381 fi
 382
 383 # Checks for libraries.
 384 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])])
 385 # Check for antlr C++ runtime (defined in config/antlr.m4)
 386 AC_LIB_ANTLR
 387
 388 # Checks for header files.
 389 AC_CHECK_HEADERS([getopt.h unistd.h])
 390
 391 # Checks for typedefs, structures, and compiler characteristics.
 392 AC_HEADER_STDBOOL
 393 AC_TYPE_UINT16_T
 394 AC_TYPE_UINT32_T
 395 AC_TYPE_UINT64_T
 396 AC_TYPE_SIZE_T
 397
 398 # Checks for library functions.
 399 # (empty)
 400
 401 # Some definitions for config.h
 402 # (empty)
 403
 404 # Prepare configure output
 405
 406 if test "$enable_shared" = yes; then BUILDING_SHARED=1; fi
 407 if test "$enable_static" = yes; then BUILDING_STATIC=1; fi
 408 AC_SUBST(BUILDING_SHARED)
 409 AC_SUBST(BUILDING_STATIC)
 410
 411 AC_SUBST(CVC4_LIBRARY_VERSION)
 412 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
 413
 414 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
 415 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
 416 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
 417 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
 418
 419 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS"
 420 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
 421 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 422
 423 # mk_include
 424 #
 425 # When automake scans Makefiles, it complains about non-standard make
 426 # features (including GNU extensions), and breaks GNU Make's
 427 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
 428 # constructs.  automake even follows "include" and messes with
 429 # included Makefiles.
 430 #
 431 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
 432 # have to hide some included Makefiles with GNU extensions.  We do
 433 # this by defining mk_include as an autoconf substitution and then
 434 # using "@mk_include@ other_makefile" in Makefile.am to include
 435 # makefiles with GNU extensions; this hides them from automake.
 436 mk_include=include
 437 AC_SUBST(mk_include)
 438
 439 AC_CONFIG_FILES([
 440   Makefile.builds
 441   Makefile]
 442   m4_esyscmd([find contrib/ doc/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,'])
 443 )
 444
 445 AC_OUTPUT
 446
 447 # Final information to the user
 448
 449 if test "$custom_build_profile" = yes; then
 450   if test "$with_build" = default; then
 451     with_build=custom
 452   else
 453     AC_MSG_WARN([])
 454     AC_MSG_WARN([This is a customized $with_build build profile.])
 455     AC_MSG_WARN([])
 456     with_build="$with_build-custom"
 457   fi
 458 fi
 459
 460 support_unit_tests='cxxtest not found; unit tests not supported'
 461 if test -n "$CXXTEST"; then
 462   support_unit_tests='unit testing infrastructure enabled in build directory'
 463 fi
 464
 465 cat <<EOF
 466
 467 CVC4 $VERSION
 468
 469 Build profile: $with_build
 470 Build ID     : $build_type
 471 Optimized    : $enable_optimized
 472 Debug symbols: $enable_debug_symbols
 473 Assertions   : $enable_assertions
 474 Tracing      : $enable_tracing
 475 Muzzle       : $enable_muzzle
 476 gcov support : $enable_coverage
 477 gprof support: $enable_profiling
 478 unit tests   : $support_unit_tests
 479
 480 CPPFLAGS     : $CPPFLAGS
 481 CXXFLAGS     : $CXXFLAGS
 482 LDFLAGS      : $LDFLAGS
 483
 484 libcvc4 version      : $CVC4_LIBRARY_VERSION
 485 libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION
 486
 487 Now just type make, followed by make check or make install, as you like.
 488
 489 EOF