Changes to configure.ac from code review

1 files changed, 102 insertions, 32 deletions

diff --git a/configure.ac b/configure.ac
index f16844f4d..80fc73fdd 100644
--- a/configure.ac
+++ b/configure.ac
@@ -1,6 +1,7 @@
 #                                               -*- Autoconf -*-
 # Process this file with autoconf to produce a configure script.
 
+dnl Preprocess CL args. Defined in config/cvc4.m4
 CVC4_AC_INIT
 
 AC_PREREQ(2.64)
@@ -10,6 +11,25 @@ AC_CONFIG_AUX_DIR([config])
 AC_CONFIG_MACRO_DIR([config])
 
 CVC4_RELEASE=prerelease
+
+# Libtool version numbers for libraries
+# Version numbers are in the form current:revision:age
+#
+# current -
+#   increment if interfaces have been added, removed or changed
+# revision -
+#   increment if source code has changed
+#   set to zero if current is incremented
+# age -
+#   increment if interfaces have been added
+#   set to zero if interfaces have been removed
+#   or changed
+#
+# For more information, see:
+# http://www.gnu.org/software/libtool/manual/libtool.html#Versioning
+# For guidance on when to change the version number, refer to the 
+# developer's guide.
+
 CVC4_LIBRARY_RELEASE_CODE=0:0:0
 CVC4_LIBRARY_VERSION=0:0:0
 CVC4_PARSER_LIBRARY_VERSION=0:0:0
@@ -27,14 +47,17 @@ AC_CANONICAL_TARGET
 
 # Features requested by the user
 AC_MSG_CHECKING([for requested build profile])
-AC_ARG_WITH([build],             [AS_HELP_STRING([--with-build=profile],     [for profile in {production,debug,default,competition}])])
+AC_ARG_WITH([build],
+  [AS_HELP_STRING([--with-build=profile],
+     [for profile in {production,debug,default,competition}])])
+
 if test -z "${with_build+set}" -o "$with_build" = default; then
   with_build=default
 fi
 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
-  non_standard_build_profile=no
+  custom_build_profile=no
 else
-  non_standard_build_profile=yes
+  custom_build_profile=yes
 fi
 btargs=
 if test -n "${enable_optimized+set}"; then
@@ -90,7 +113,7 @@ AC_MSG_RESULT([$with_build])
 
 AC_MSG_CHECKING([for appropriate build string])
 build_type=`$ac_confdir/config/build-type $with_build $btargs`
-if test "$non_standard_build_profile" = yes; then
+if test "$custom_build_profile" = yes; then
   if test "$with_build" = default; then
     build_type=`$ac_confdir/config/build-type custom $btargs`
   fi
@@ -120,8 +143,10 @@ else
   AC_MSG_RESULT([this one (user-specified)])
 fi
 
+# Unpack standard build types. Any particular options can be overriden with
+# --enable/disable-X options
 case "$with_build" in
-  production)
+  production) # highly optimized, no assertions, no tracing
     CVC4CPPFLAGS=
     CVC4CXXFLAGS=-O3
     CVC4LDFLAGS=
@@ -129,7 +154,7 @@ case "$with_build" in
     if test -z "${enable_tracing+set}"   ; then enable_tracing=no                ; fi
     if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
     ;;
-  debug)
+  debug) # Unoptimized, debug symbols, assertions, tracing
     CVC4CPPFLAGS=-DCVC4_DEBUG
     CVC4CXXFLAGS='-O0 -fno-inline -ggdb3'
     CVC4LDFLAGS=
@@ -137,7 +162,7 @@ case "$with_build" in
     if test -z "${enable_tracing+set}"   ; then enable_tracing=yes               ; fi
     if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
     ;;
-  default)
+  default) # moderately optimized, assertions, tracing
     CVC4CPPFLAGS=
     CVC4CXXFLAGS=-O2
     CVC4LDFLAGS=
@@ -145,7 +170,7 @@ case "$with_build" in
     if test -z "${enable_tracing+set}"   ; then enable_tracing=yes               ; fi
     if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
     ;;
-  competition)
+  competition) # maximally optimized, no assertions, no tracing, muzzled
     CVC4CPPFLAGS=
     CVC4CXXFLAGS='-O9 -funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
     CVC4LDFLAGS=
@@ -159,72 +184,111 @@ case "$with_build" in
 esac
 
 AC_MSG_CHECKING([whether to optimize libcvc4])
-AC_ARG_ENABLE([optimized],       [AS_HELP_STRING([--enable-optimized],       [optimize the build])])
+
+AC_ARG_ENABLE([optimized],
+  [AS_HELP_STRING([--enable-optimized],       
+     [optimize the build])])
+
 if test -z "${enable_optimized+set}"; then
   enable_optimized=no
 fi
+
 AC_MSG_RESULT([$enable_optimized])
+
 if test "$enable_optimized" = yes; then
   CVC4CXXFLAGS="$CVC4CXXFLAGS -O3"
 fi
 
 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
-AC_ARG_ENABLE([debug-symbols],   [AS_HELP_STRING([--disable-debug-symbols],  [do not include debug symbols in libcvc4])])
+
+AC_ARG_ENABLE([debug-symbols],   
+  [AS_HELP_STRING([--disable-debug-symbols],  
+     [do not include debug symbols in libcvc4])])
+
 if test -z "${enable_debug_symbols+set}"; then
   enable_debug_symbols=yes
 fi
+
 AC_MSG_RESULT([$enable_debug_symbols])
+
 if test "$enable_debug_symbols" = yes; then
   CVC4CXXFLAGS="$CVC4CXXFLAGS -ggdb3"
 fi
 
 AC_MSG_CHECKING([whether to include assertions in build])
-AC_ARG_ENABLE([assertions],      [AS_HELP_STRING([--disable-assertions],     [turn off assertions in build])])
+
+AC_ARG_ENABLE([assertions],      
+  [AS_HELP_STRING([--disable-assertions],     
+     [turn off assertions in build])])
+
 if test -z "${enable_assertions+set}"; then
   enable_assertions=yes
 fi
+
 AC_MSG_RESULT([$enable_assertions])
+
 if test "$enable_assertions" = yes; then
   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_ASSERTIONS"
 fi
 
 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
-AC_ARG_ENABLE([tracing],         [AS_HELP_STRING([--disable-tracing],        [remove all tracing code from CVC4])])
+AC_ARG_ENABLE([tracing],         
+  [AS_HELP_STRING([--disable-tracing],        
+     [remove all tracing code from CVC4])])
+
 if test -z "${enable_tracing+set}"; then
   enable_tracing=yes
 fi
+
 AC_MSG_RESULT([$enable_tracing])
+
 if test "$enable_tracing" = yes; then
   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_TRACING"
 fi
 
 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
-AC_ARG_ENABLE([muzzle],          [AS_HELP_STRING([--enable-muzzle],          [completely silence CVC4; remove ALL non-result output from build])])
+AC_ARG_ENABLE([muzzle],          
+  [AS_HELP_STRING([--enable-muzzle],          
+     [completely silence CVC4; remove ALL non-result output from build])])
+
 if test -z "${enable_muzzle+set}"; then
   enable_muzzle=no
 fi
+
 AC_MSG_RESULT([$enable_muzzle])
+
 if test "$enable_muzzle" = yes; then
   CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_MUZZLE"
 fi
 
 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
-AC_ARG_ENABLE([coverage],        [AS_HELP_STRING([--enable-coverage],        [build with support for gcov coverage testing])])
+AC_ARG_ENABLE([coverage],        
+  [AS_HELP_STRING([--enable-coverage],        
+     [build with support for gcov coverage testing])])
+
 if test -z "${enable_coverage+set}"; then
   enable_coverage=no
 fi
+
 AC_MSG_RESULT([$enable_coverage])
+
 if test "$enable_coverage" = yes; then
   CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage"
   CVC4LDFLAGS="$CVC4LDFLAGS --coverage"
 fi
 
 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
-AC_ARG_ENABLE([profiling],       [AS_HELP_STRING([--enable-profiling],       [build with support for gprof profiling])])
+
+AC_ARG_ENABLE([profiling],       
+  [AS_HELP_STRING([--enable-profiling],       
+     [build with support for gprof profiling])])
+
 if test -z "${enable_profiling+set}"; then
   enable_profiling=no
 fi
+
 AC_MSG_RESULT([$enable_profiling])
+
 if test "$enable_profiling" = yes; then
   CVC4CXXFLAGS="$CVC4CXXFLAGS -pg"
   CVC4LDFLAGS="$CVC4LDFLAGS -pg"
@@ -245,9 +309,12 @@ AC_MSG_CHECKING([for user LDFLAGS])
 if test -z "${LDFLAGS+set}" ; then user_ldflags=no ; else user_ldflags=yes ; fi
 AC_MSG_RESULT([${LDFLAGS-none}])
 
+# Initialize libtools configuration options.
+
 _LT_SET_OPTION([LT_INIT],[win32-dll])
-LT_INIT
 
+dnl defined in config/libtools.m4
+LT_INIT
 
 # Checks for programs.
 AC_PROG_CC
@@ -257,17 +324,19 @@ AC_PROG_INSTALL
 AC_PROG_ANTLR
 
 AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, [])
+
 if test -z "$DOXYGEN"; then
   AC_MSG_WARN([documentation targets require doxygen.  Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.])
 fi
+
 AC_ARG_VAR(DOXYGEN, [location of doxygen binary])
 
 AC_SUBST([CXXTEST])
+
 AC_ARG_WITH([cxxtest-dir], 
   [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
   [CXXTEST="$withval"])
 
-dnl AC_ARG_VAR(CXXTEST, [path to cxxtest installation])
 CXXTESTGEN=
 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
 if test -z "$CXXTESTGEN"; then
@@ -284,14 +353,22 @@ elif test -z "$CXXTEST"; then
     CXXTEST=
   fi
 fi
+
 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
 
 AC_ARG_VAR(TEST_CPPFLAGS, [CXXFLAGS to use when testing (default=$CPPFLAGS)])
 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
 AC_ARG_VAR(TEST_LDFLAGS,  [LDFLAGS to use when testing (default=$LDFLAGS)])
 
+AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
+
 if test -n "$CXXTEST"; then
-  AC_CHECK_PROG(PERL, perl, perl, [])
+  if test -z "$PERL"; then
+    AC_CHECK_PROGS(PERL, perl, perl, [])
+  else
+    AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
+  fi
+
   if test -z "$PERL"; then
     AC_MSG_WARN([unit tests disabled, perl not found.])
     CXXTESTGEN=
@@ -304,7 +381,6 @@ AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmp
 # Check for antlr C++ runtime (defined in config/antlr.m4)
 AC_LIB_ANTLR
 
-
 # Checks for header files.
 AC_CHECK_HEADERS([getopt.h unistd.h])
 
@@ -316,14 +392,17 @@ AC_TYPE_UINT64_T
 AC_TYPE_SIZE_T
 
 # Checks for library functions.
+# (empty)
 
 # Some definitions for config.h
+# (empty)
 
 # Prepare configure output
 
 AC_SUBST(CVC4_LIBRARY_RELEASE_CODE)
 AC_SUBST(CVC4_LIBRARY_VERSION)
 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
+
 if test "$user_cppflags" = no; then
   CPPFLAGS="$CVC4CPPFLAGS"
 fi
@@ -365,15 +444,14 @@ AC_OUTPUT
 
 # Final information to the user
 
-non_standard=
-if test "$non_standard_build_profile" = yes; then
+if test "$custom_build_profile" = yes; then
   if test "$with_build" = default; then
     with_build=custom
   else
     AC_MSG_WARN([])
-    AC_MSG_WARN([This is a non-standard $with_build build profile.])
+    AC_MSG_WARN([This is a customized $with_build build profile.])
     AC_MSG_WARN([])
-    non_standard=-custom
+    with_build="$with_build-custom"
   fi
 fi
 
@@ -386,7 +464,7 @@ cat <<EOF
 
 CVC4 $VERSION
 
-Build profile: $with_build$non_standard
+Build profile: $with_build
 Build ID     : $build_type
 Optimized    : $enable_optimized
 Debug symbols: $enable_debug_symbols
@@ -433,11 +511,3 @@ if test "$user_ldflags" = yes; then
   AC_MSG_WARN([    $CVC4LDFLAGS])
   AC_MSG_WARN([])
 fi
-
-if test "$non_standard_build_profile" = yes; then
-  if test "$with_build" = default; then :; else
-    AC_MSG_WARN([])
-    AC_MSG_WARN([This is a non-standard $with_build build profile.])
-    AC_MSG_WARN([])
-  fi
-fi