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   CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage"
 303   CVC4LDFLAGS="$CVC4LDFLAGS --coverage"
 304 fi
 305
 306 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
 307
 308 AC_ARG_ENABLE([profiling],
 309   [AS_HELP_STRING([--enable-profiling],
 310      [build with support for gprof profiling])])
 311
 312 if test -z "${enable_profiling+set}"; then
 313   enable_profiling=no
 314 fi
 315
 316 AC_MSG_RESULT([$enable_profiling])
 317
 318 if test "$enable_profiling" = yes; then
 319   CVC4CXXFLAGS="$CVC4CXXFLAGS -pg"
 320   CVC4LDFLAGS="$CVC4LDFLAGS -pg"
 321 fi
 322
 323 AM_INIT_AUTOMAKE(cvc4, $CVC4_RELEASE_STRING)
 324 AC_CONFIG_HEADERS([config.h])
 325
 326 # Initialize libtool's configuration options.
 327 _LT_SET_OPTION([LT_INIT],[win32-dll])
 328 LT_INIT
 329
 330 # Checks for programs.
 331 AC_PROG_CC
 332 AC_PROG_CXX
 333 AC_PROG_INSTALL
 334 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 335 AC_PROG_ANTLR
 336
 337 DX_PDF_FEATURE(OFF)
 338 DX_PS_FEATURE(OFF)
 339 DX_DOT_FEATURE(OFF)
 340 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc)
 341
 342 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
 343
 344 AC_SUBST([CXXTEST])
 345
 346 AC_ARG_WITH([cxxtest-dir],
 347   [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
 348   [CXXTEST="$withval"])
 349
 350 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
 351 # relative path) and having switched the configure directory (see above),
 352 # search with respect to the top source dir, not the build dir
 353 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
 354   case "$CXXTEST" in
 355     /*) ;;
 356     *)  CXXTEST="$srcdir/$CXXTEST" ;;
 357   esac
 358 fi
 359
 360 CXXTESTGEN=
 361 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
 362 if test -z "$CXXTESTGEN"; then
 363   AC_MSG_NOTICE([unit tests disabled, cxxtestgen.pl not found.])
 364 elif test -z "$CXXTEST"; then
 365   CXXTEST=$(dirname "$CXXTESTGEN")
 366   AC_MSG_CHECKING([for location of CxxTest headers])
 367   if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
 368     AC_MSG_RESULT([$CXXTEST])
 369   else
 370     AC_MSG_RESULT([not found])
 371     AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
 372     CXXTESTGEN=
 373     CXXTEST=
 374   fi
 375 fi
 376
 377 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
 378
 379 AC_ARG_VAR(TEST_CPPFLAGS, [CXXFLAGS to use when testing (default=$CPPFLAGS)])
 380 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
 381 AC_ARG_VAR(TEST_LDFLAGS,  [LDFLAGS to use when testing (default=$LDFLAGS)])
 382
 383 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
 384
 385 if test -n "$CXXTEST"; then
 386   if test -z "$PERL"; then
 387     AC_CHECK_PROGS(PERL, perl, perl, [])
 388   else
 389     AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
 390   fi
 391
 392   if test -z "$PERL"; then
 393     AC_MSG_WARN([unit tests disabled, perl not found.])
 394     CXXTESTGEN=
 395     CXXTEST=
 396   fi
 397 fi
 398
 399 # Checks for libraries.
 400 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])])
 401 # Check for antlr C++ runtime (defined in config/antlr.m4)
 402 AC_LIB_ANTLR
 403
 404 # Checks for header files.
 405 AC_CHECK_HEADERS([getopt.h unistd.h])
 406
 407 # Checks for typedefs, structures, and compiler characteristics.
 408 #AC_HEADER_STDBOOL
 409 AC_TYPE_UINT16_T
 410 AC_TYPE_UINT32_T
 411 AC_TYPE_UINT64_T
 412 AC_TYPE_SIZE_T
 413
 414 # Checks for library functions.
 415 # (empty)
 416
 417 # Some definitions for config.h
 418 # (empty)
 419
 420 # Prepare configure output
 421
 422 if test "$enable_shared" = yes; then BUILDING_SHARED=1; fi
 423 if test "$enable_static" = yes; then BUILDING_STATIC=1; fi
 424 AC_SUBST(BUILDING_SHARED)
 425 AC_SUBST(BUILDING_STATIC)
 426 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
 427
 428 AC_SUBST(CVC4_LIBRARY_VERSION)
 429 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
 430
 431 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
 432 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
 433 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
 434 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
 435
 436 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS"
 437 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
 438 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 439
 440 # mk_include
 441 #
 442 # When automake scans Makefiles, it complains about non-standard make
 443 # features (including GNU extensions), and breaks GNU Make's
 444 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
 445 # constructs.  automake even follows "include" and messes with
 446 # included Makefiles.
 447 #
 448 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
 449 # have to hide some included Makefiles with GNU extensions.  We do
 450 # this by defining mk_include as an autoconf substitution and then
 451 # using "@mk_include@ other_makefile" in Makefile.am to include
 452 # makefiles with GNU extensions; this hides them from automake.
 453 mk_include=include
 454 AC_SUBST(mk_include)
 455
 456 AC_CONFIG_FILES([
 457   Makefile.builds
 458   Makefile]
 459   m4_esyscmd([find contrib/ doc/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,'])
 460 )
 461
 462 AC_OUTPUT
 463
 464 # Final information to the user
 465
 466 if test "$custom_build_profile" = yes; then
 467   if test "$with_build" = default; then
 468     with_build=custom
 469   else
 470     AC_MSG_WARN([])
 471     AC_MSG_WARN([This is a customized $with_build build profile.])
 472     AC_MSG_WARN([])
 473     with_build="$with_build-custom"
 474   fi
 475 fi
 476
 477 support_unit_tests='cxxtest not found; unit tests not supported'
 478 if test -n "$CXXTEST"; then
 479   support_unit_tests='unit testing infrastructure enabled in build directory'
 480 fi
 481
 482 cat <<EOF
 483
 484 CVC4 $VERSION
 485
 486 Build profile: $with_build
 487 Build ID     : $build_type
 488 Optimized    : $enable_optimized
 489 Debug symbols: $enable_debug_symbols
 490 Assertions   : $enable_assertions
 491 Tracing      : $enable_tracing
 492 Muzzle       : $enable_muzzle
 493 gcov support : $enable_coverage
 494 gprof support: $enable_profiling
 495 unit tests   : $support_unit_tests
 496
 497 static libs  : $enable_static
 498 shared libs  : $enable_shared
 499 static binary: $enable_static_binary
 500
 501 CPPFLAGS     : $CPPFLAGS
 502 CXXFLAGS     : $CXXFLAGS
 503 LDFLAGS      : $LDFLAGS
 504
 505 libcvc4 version      : $CVC4_LIBRARY_VERSION
 506 libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION
 507
 508 Now just type make, followed by make check or make install, as you like.
 509
 510 EOF