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_RELEASE=prerelease
  14
  15 # Libtool version numbers for libraries
  16 # Version numbers are in the form current:revision:age
  17 #
  18 # current -
  19 #   increment if interfaces have been added, removed or changed
  20 # revision -
  21 #   increment if source code has changed
  22 #   set to zero if current is incremented
  23 # age -
  24 #   increment if interfaces have been added
  25 #   set to zero if interfaces have been removed
  26 #   or changed
  27 #
  28 # For more information, see:
  29 # http://www.gnu.org/software/libtool/manual/libtool.html#Versioning
  30 # For guidance on when to change the version number, refer to the
  31 # developer's guide.
  32
  33 CVC4_LIBRARY_VERSION=0:0:0
  34 CVC4_PARSER_LIBRARY_VERSION=0:0:0
  35
  36 # Using the AC_CANONICAL_* macros destroy the command line you get
  37 # from $@, which we want later for determining the build profile.  So
  38 # we save it.  (We can't do our build profile stuff here, or it's not
  39 # included in the output... autoconf overrides us on the orderings of
  40 # some things.)
  41 config_cmdline="$@"
  42
  43 # turn off static lib building by default
  44 AC_ENABLE_SHARED
  45 AC_DISABLE_STATIC
  46
  47 AC_CANONICAL_BUILD
  48 AC_CANONICAL_HOST
  49 AC_CANONICAL_TARGET
  50
  51 # Features requested by the user
  52 AC_MSG_CHECKING([for requested build profile])
  53 AC_ARG_WITH([build],
  54   [AS_HELP_STRING([--with-build=profile],
  55      [for profile in {production,debug,default,competition}])])
  56
  57 if test -z "${with_build+set}" -o "$with_build" = default; then
  58   with_build=default
  59 fi
  60 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
  61   custom_build_profile=no
  62 else
  63   custom_build_profile=yes
  64 fi
  65 btargs=
  66 if test -n "${enable_optimized+set}"; then
  67   if test "$enable_optimized" = yes; then
  68     btargs="$btargs optimized"
  69   else
  70     btargs="$btargs nooptimized"
  71   fi
  72 fi
  73 if test -n "${enable_debug_symbols+set}"; then
  74   if test "$enable_debug_symbols" = yes; then
  75     btargs="$btargs debugsymbols"
  76   else
  77     btargs="$btargs nodebugsymbols"
  78   fi
  79 fi
  80 if test -n "${enable_assertions+set}"; then
  81   if test "$enable_assertions" = yes; then
  82     btargs="$btargs assertions"
  83   else
  84     btargs="$btargs noassertions"
  85   fi
  86 fi
  87 if test -n "${enable_tracing+set}"; then
  88   if test "$enable_tracing" = yes; then
  89     btargs="$btargs tracing"
  90   else
  91     btargs="$btargs notracing"
  92   fi
  93 fi
  94 if test -n "${enable_muzzle+set}"; then
  95   if test "$enable_muzzle" = yes; then
  96     btargs="$btargs muzzle"
  97   else
  98     btargs="$btargs nomuzzle"
  99   fi
 100 fi
 101 if test -n "${enable_coverage+set}"; then
 102   if test "$enable_coverage" = yes; then
 103     btargs="$btargs coverage"
 104   else
 105     btargs="$btargs nocoverage"
 106   fi
 107 fi
 108 if test -n "${enable_profiling+set}"; then
 109   if test "$enable_profiling" = yes; then
 110     btargs="$btargs profiling"
 111   else
 112     btargs="$btargs noprofiling"
 113   fi
 114 fi
 115 AC_MSG_RESULT([$with_build])
 116
 117 AC_MSG_CHECKING([for appropriate build string])
 118 build_type=`$ac_confdir/config/build-type $with_build $btargs`
 119 if test "$custom_build_profile" = yes; then
 120   if test "$with_build" = default; then
 121     build_type=`$ac_confdir/config/build-type custom $btargs`
 122   fi
 123 fi
 124 AC_MSG_RESULT($build_type)
 125
 126 # Require building in target and build-specific build directory:
 127 #
 128 # If the configure script is invoked from the top-level source
 129 # directory, it creates a suitable build directory (based on the build
 130 # architecture and build profile from $build_type), changes into it,
 131 # and reinvokes itself.  CVC4_CONFIGURE_IN_BUILDS is an envariable
 132 # that breaks any possibility of infinite recursion in this process.
 133 AC_MSG_CHECKING([what dir to configure])
 134 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
 135   AC_MSG_RESULT([this one (in builds/)])
 136 elif test -e src/include/cvc4_config.h; then
 137   AC_MSG_RESULT([builds/$target/$build_type])
 138   echo
 139   if test -z "$ac_srcdir"; then
 140     mkbuilddir=./config/mkbuilddir
 141   else
 142     mkbuilddir=$ac_srcdir/config/mkbuilddir
 143   fi
 144   echo $mkbuilddir "$target" "$build_type"
 145   $mkbuilddir "$target" "$build_type"
 146   echo cd "builds/$target/$build_type"
 147   cd "builds/$target/$build_type"
 148   CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
 149   echo ../../../configure $config_cmdline
 150   exec ../../../configure $config_cmdline
 151 else
 152   AC_MSG_RESULT([this one (user-specified)])
 153 fi
 154
 155 # Unpack standard build types. Any particular options can be overriden with
 156 # --enable/disable-X options
 157 case "$with_build" in
 158   production) # highly optimized, no assertions, no tracing
 159     CVC4CPPFLAGS=
 160     CVC4CXXFLAGS=-O3
 161     CVC4LDFLAGS=
 162     if test -z "${enable_assertions+set}"; then enable_assertions=no             ; fi
 163     if test -z "${enable_tracing+set}"   ; then enable_tracing=no                ; fi
 164     if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
 165     ;;
 166   debug) # Unoptimized, debug symbols, assertions, tracing
 167     CVC4CPPFLAGS=-DCVC4_DEBUG
 168     CVC4CXXFLAGS='-O0 -fno-inline -ggdb3'
 169     CVC4LDFLAGS=
 170     if test -z "${enable_assertions+set}"; then enable_assertions=yes            ; fi
 171     if test -z "${enable_tracing+set}"   ; then enable_tracing=yes               ; fi
 172     if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
 173     ;;
 174   default) # moderately optimized, assertions, tracing
 175     CVC4CPPFLAGS=
 176     CVC4CXXFLAGS=-O2
 177     CVC4LDFLAGS=
 178     if test -z "${enable_assertions+set}"; then enable_assertions=yes            ; fi
 179     if test -z "${enable_tracing+set}"   ; then enable_tracing=yes               ; fi
 180     if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
 181     ;;
 182   competition) # maximally optimized, no assertions, no tracing, muzzled
 183     CVC4CPPFLAGS=
 184     CVC4CXXFLAGS='-O9 -funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
 185     CVC4LDFLAGS=
 186     if test -z "${enable_assertions+set}"; then enable_assertions=no             ; fi
 187     if test -z "${enable_tracing+set}"   ; then enable_tracing=no                ; fi
 188     if test -z "${enable_muzzle+set}"    ; then enable_muzzle=yes                ; fi
 189     ;;
 190   *)
 191     AC_MSG_FAILURE([unknown build profile: $with_build])
 192     ;;
 193 esac
 194
 195 AC_MSG_CHECKING([whether to optimize libcvc4])
 196
 197 AC_ARG_ENABLE([optimized],
 198   [AS_HELP_STRING([--enable-optimized],
 199      [optimize the build])])
 200
 201 if test -z "${enable_optimized+set}"; then
 202   enable_optimized=no
 203 fi
 204
 205 AC_MSG_RESULT([$enable_optimized])
 206
 207 if test "$enable_optimized" = yes; then
 208   CVC4CXXFLAGS="$CVC4CXXFLAGS -O3"
 209 fi
 210
 211 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
 212
 213 AC_ARG_ENABLE([debug-symbols],
 214   [AS_HELP_STRING([--disable-debug-symbols],
 215      [do not include debug symbols in libcvc4])])
 216
 217 if test -z "${enable_debug_symbols+set}"; then
 218   enable_debug_symbols=yes
 219 fi
 220
 221 AC_MSG_RESULT([$enable_debug_symbols])
 222
 223 if test "$enable_debug_symbols" = yes; then
 224   CVC4CXXFLAGS="$CVC4CXXFLAGS -ggdb3"
 225 fi
 226
 227 AC_MSG_CHECKING([whether to include assertions in build])
 228
 229 AC_ARG_ENABLE([assertions],
 230   [AS_HELP_STRING([--disable-assertions],
 231      [turn off assertions in build])])
 232
 233 if test -z "${enable_assertions+set}"; then
 234   enable_assertions=yes
 235 fi
 236
 237 AC_MSG_RESULT([$enable_assertions])
 238
 239 if test "$enable_assertions" = yes; then
 240   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_ASSERTIONS"
 241 fi
 242
 243 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
 244 AC_ARG_ENABLE([tracing],
 245   [AS_HELP_STRING([--disable-tracing],
 246      [remove all tracing code from CVC4])])
 247
 248 if test -z "${enable_tracing+set}"; then
 249   enable_tracing=yes
 250 fi
 251
 252 AC_MSG_RESULT([$enable_tracing])
 253
 254 if test "$enable_tracing" = yes; then
 255   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_TRACING"
 256 fi
 257
 258 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
 259 AC_ARG_ENABLE([muzzle],
 260   [AS_HELP_STRING([--enable-muzzle],
 261      [completely silence CVC4; remove ALL non-result output from build])])
 262
 263 if test -z "${enable_muzzle+set}"; then
 264   enable_muzzle=no
 265 fi
 266
 267 AC_MSG_RESULT([$enable_muzzle])
 268
 269 if test "$enable_muzzle" = yes; then
 270   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_MUZZLE"
 271 fi
 272
 273 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
 274 AC_ARG_ENABLE([coverage],
 275   [AS_HELP_STRING([--enable-coverage],
 276      [build with support for gcov coverage testing])])
 277
 278 if test -z "${enable_coverage+set}"; then
 279   enable_coverage=no
 280 fi
 281
 282 AC_MSG_RESULT([$enable_coverage])
 283
 284 if test "$enable_coverage" = yes; then
 285   CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage"
 286   CVC4LDFLAGS="$CVC4LDFLAGS --coverage"
 287 fi
 288
 289 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
 290
 291 AC_ARG_ENABLE([profiling],
 292   [AS_HELP_STRING([--enable-profiling],
 293      [build with support for gprof profiling])])
 294
 295 if test -z "${enable_profiling+set}"; then
 296   enable_profiling=no
 297 fi
 298
 299 AC_MSG_RESULT([$enable_profiling])
 300
 301 if test "$enable_profiling" = yes; then
 302   CVC4CXXFLAGS="$CVC4CXXFLAGS -pg"
 303   CVC4LDFLAGS="$CVC4LDFLAGS -pg"
 304 fi
 305
 306 AM_INIT_AUTOMAKE(cvc4, $CVC4_RELEASE)
 307 AC_CONFIG_HEADERS([config.h])
 308
 309 # Initialize libtool's configuration options.
 310 _LT_SET_OPTION([LT_INIT],[win32-dll])
 311 LT_INIT
 312
 313 # Checks for programs.
 314 AC_PROG_CC
 315 AC_PROG_CXX
 316 AC_PROG_INSTALL
 317 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 318 AC_PROG_ANTLR
 319
 320 AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, [])
 321
 322 if test -z "$DOXYGEN"; then
 323   AC_MSG_WARN([documentation targets require doxygen.  Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.])
 324 fi
 325
 326 AC_ARG_VAR(DOXYGEN, [location of doxygen binary])
 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 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS"
 415 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
 416 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 417
 418 # mk_include
 419 #
 420 # When automake scans Makefiles, it complains about non-standard make
 421 # features (including GNU extensions), and breaks GNU Make's
 422 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
 423 # constructs.  automake even follows "include" and messes with
 424 # included Makefiles.
 425 #
 426 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
 427 # have to hide some included Makefiles with GNU extensions.  We do
 428 # this by defining mk_include as an autoconf substitution and then
 429 # using "@mk_include@ other_makefile" in Makefile.am to include
 430 # makefiles with GNU extensions; this hides them from automake.
 431 mk_include=include
 432 AC_SUBST(mk_include)
 433
 434 AC_CONFIG_FILES([
 435   Makefile.builds
 436   Makefile]
 437   m4_esyscmd([find contrib/ doc/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,'])
 438 )
 439
 440 AC_OUTPUT
 441
 442 # Final information to the user
 443
 444 if test "$custom_build_profile" = yes; then
 445   if test "$with_build" = default; then
 446     with_build=custom
 447   else
 448     AC_MSG_WARN([])
 449     AC_MSG_WARN([This is a customized $with_build build profile.])
 450     AC_MSG_WARN([])
 451     with_build="$with_build-custom"
 452   fi
 453 fi
 454
 455 support_unit_tests='cxxtest not found; unit tests not supported'
 456 if test -n "$CXXTEST"; then
 457   support_unit_tests='unit testing infrastructure enabled in build directory'
 458 fi
 459
 460 cat <<EOF
 461
 462 CVC4 $VERSION
 463
 464 Build profile: $with_build
 465 Build ID     : $build_type
 466 Optimized    : $enable_optimized
 467 Debug symbols: $enable_debug_symbols
 468 Assertions   : $enable_assertions
 469 Tracing      : $enable_tracing
 470 Muzzle       : $enable_muzzle
 471 gcov support : $enable_coverage
 472 gprof support: $enable_profiling
 473 unit tests   : $support_unit_tests
 474
 475 CPPFLAGS     : $CPPFLAGS
 476 CXXFLAGS     : $CXXFLAGS
 477 LDFLAGS      : $LDFLAGS
 478
 479 libcvc4 version      : $CVC4_LIBRARY_VERSION
 480 libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION
 481
 482 Now just type make, followed by make check or make install, as you like.
 483
 484 EOF