From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 17 Dec 2009 00:02:12 +0000 (+0000)
Subject: support nonstandard, unconfigured builds (e.g., "./configure debug" followed by ... 
X-Git-Tag: cvc5-1.0.0~9369
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=73fd355fd1a9f6cacfc3170d29e29fccc94ab539;p=cvc5.git

support nonstandard, unconfigured builds (e.g., "./configure debug" followed by "make production ASSERTIONS=1")
---

diff --git a/Makefile.am b/Makefile.am
index 76130be45..07a91f21a 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -5,8 +5,15 @@ ACLOCAL_AMFLAGS = -I config
 
 SUBDIRS = src test doc contrib
 
+@mk_include@ @top_srcdir@/Makefile.reconf_args
+
 .PHONY: production debug default competition
-production: ; (cd @top_srcdir@ && ./configure --with-build=production && $(MAKE))
-debug:      ; (cd @top_srcdir@ && ./configure --with-build=debug && $(MAKE))
-default:    ; (cd @top_srcdir@ && ./configure --with-build=default && $(MAKE))
-competition:; (cd @top_srcdir@ && ./configure --with-build=competition && $(MAKE))
+production debug default competition:
+	cd @top_srcdir@; \
+	dir="builds/`config/config.guess`/`config/build-type $@ $(BTARGS)`"; \
+	if test -e "$$dir"; then \
+		cd "$$dir" && $(MAKE); \
+	else \
+		./configure --with-build=$@ $(CONFARGS) && $(MAKE); \
+	fi
+
diff --git a/Makefile.in b/Makefile.in
index 6beb31597..139f43cc0 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -226,6 +226,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
@@ -744,11 +745,17 @@ uninstall-am:
 	ps ps-am tags tags-recursive uninstall uninstall-am
 
 
+@mk_include@ @top_srcdir@/Makefile.reconf_args
+
 .PHONY: production debug default competition
-production: ; (cd @top_srcdir@ && ./configure --with-build=production && $(MAKE))
-debug:      ; (cd @top_srcdir@ && ./configure --with-build=debug && $(MAKE))
-default:    ; (cd @top_srcdir@ && ./configure --with-build=default && $(MAKE))
-competition:; (cd @top_srcdir@ && ./configure --with-build=competition && $(MAKE))
+production debug default competition:
+	cd @top_srcdir@; \
+	dir="builds/`config/config.guess`/`config/build-type $@ $(BTARGS)`"; \
+	if test -e "$$dir"; then \
+		cd "$$dir" && $(MAKE); \
+	else \
+		./configure --with-build=$@ $(CONFARGS) && $(MAKE); \
+	fi
 
 # Tell versions [3.59,3.63) of GNU make to not export all variables.
 # Otherwise a system limit (for SysV at least) may be exceeded.
diff --git a/Makefile.reconf_args b/Makefile.reconf_args
new file mode 100644
index 000000000..10d3c84b9
--- /dev/null
+++ b/Makefile.reconf_args
@@ -0,0 +1,77 @@
+# This makefile snippet maps make-time arguments to configure and
+# build-type arguments
+#
+# Morgan Deters <mdeters@cs.nyu.edu> 2009 for CVC4
+BTARGS =
+CONFARGS =
+
+ifeq ($(OPTIMIZE),0)
+  BTARGS += noopt
+  CONFARGS += --disable-optimized
+else
+ifeq ($(OPTIMIZE),1)
+  BTARGS += opt
+  CONFARGS += --enable-optimized
+endif
+endif
+
+ifeq ($(DEBUG_SYMBOLS),0)
+  BTARGS += nodsy
+  CONFARGS += --disable-debug-symbols
+else
+ifeq ($(DEBUG_SYMBOLS),1)
+  BTARGS += dsy
+  CONFARGS += --enable-debug-symbols
+endif
+endif
+
+ifeq ($(ASSERTIONS),0)
+  BTARGS += noass
+  CONFARGS += --disable-assertions
+else
+ifeq ($(ASSERTIONS),1)
+  BTARGS += ass
+  CONFARGS += --enable-assertions
+endif
+endif
+
+ifeq ($(TRACING),0)
+  BTARGS += notrc
+  CONFARGS += --disable-tracing
+else
+ifeq ($(TRACING),1)
+  BTARGS += trc
+  CONFARGS += --enable-tracing
+endif
+endif
+
+ifeq ($(MUZZLE),0)
+  BTARGS += nomzl
+  CONFARGS += --disable-muzzle
+else
+ifeq ($(MUZZLE),1)
+  BTARGS += mzl
+  CONFARGS += --enable-muzzle
+endif
+endif
+
+ifeq ($(COVERAGE),0)
+  BTARGS += nocvg
+  CONFARGS += --disable-coverage
+else
+ifeq ($(COVERAGE),1)
+  BTARGS += cvg
+  CONFARGS += --enable-coverage
+endif
+endif
+
+ifeq ($(PROFILING),0)
+  BTARGS += noprf
+  CONFARGS += --disable-profiling
+else
+ifeq ($(PROFILING),1)
+  BTARGS += prf
+  CONFARGS += --enable-profiling
+endif
+endif
+
diff --git a/config/build-type b/config/build-type
new file mode 100755
index 000000000..997e0f8e3
--- /dev/null
+++ b/config/build-type
@@ -0,0 +1,59 @@
+#!/bin/sh
+#
+# build-type
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+#
+# usage: build-type profile [ overrides... ]
+#
+# Returns a build string for the given profile and overrides.
+# For example, "build-type debug noass" returns the canonical build
+# string for a debug build with assertions turned off.
+#
+# The default build directory for CVC4 is then (assuming a standard
+# debug build):
+#
+#   builds/`config/config.guess`/`config/build-type debug`
+#
+# This script is used both in CVC4's configure script and in the
+# top-level Makefile when you build another profile than the
+# "current" build (to see if there already was a build of that type).
+#
+# The codes for overrides are as follows:
+#
+#   opt - optimizing
+#   dsy - debug symbols
+#   ass - assertions
+#   trc - tracing
+#   mzl - muzzle
+#   cvg - coverage
+#   prf - profiling
+#
+
+if [ $# -eq 0 ]; then
+  echo "usage: build-type profile [ overrides... ]" >&2
+  exit
+fi
+
+build_type=$1
+shift
+
+while [ $# -gt 0 ]; do
+  case "$1" in
+    no*) eval `expr "$1" : 'no\(.*\)'`=0 ;;
+    *)   eval $1=1 ;;
+  esac
+  shift
+done
+
+build_type_suffix=
+for arg in opt dsy ass trc mzl cvg prf; do
+  if eval [ -n '"${'$arg'+set}"' ]; then
+    if eval [ '"${'$arg'}"' -eq 0 ]; then
+      build_type_suffix=$build_type_suffix-no$arg
+    else
+      build_type_suffix=$build_type_suffix-$arg
+    fi
+  fi
+done
+
+echo $build_type$build_type_suffix
diff --git a/config/cvc4.m4 b/config/cvc4.m4
index 1926fa54a..661631b4d 100644
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -18,7 +18,7 @@ do
   case $ac_option in
     -*|*=*) ;;
     *) ac_cvc4_build_profile_set=yes
-       AC_MSG_WARN([building profile $ac_option])
+       AC_MSG_NOTICE([CVC4: building profile $ac_option])
        ac_option="--with-build=$ac_option" ;;
   esac
   eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"$ac_option\""'
diff --git a/config/mkbuilddir b/config/mkbuilddir
new file mode 100644
index 000000000..1bc895548
--- /dev/null
+++ b/config/mkbuilddir
@@ -0,0 +1,39 @@
+#!/bin/sh
+#
+# mkbuilddir
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+#
+# usage: mkbuilddir target build-type
+#
+# Sets up the builds/ directory for building build-type for target:
+# - removes configure detritus from top-level source directory
+# - makes builds/$target/$build_type directory if it's not already there
+# - links builds/Makefile to (possibly nonexistent) build Makefile
+# - creates the builds/current Makefile include snippet
+# - links builds/src and builds/test into build directory
+#
+
+if [ $# -ne 2 ]; then
+  echo 'usage: mkbuilddir target build_type' >&2
+  exit 1
+fi
+
+target=$1
+build_type=$2
+
+echo Setting up "builds/$target/$build_type"...
+rm -fv config.log config.status confdefs.h
+mkdir -pv "builds/$target/$build_type"
+ln -sfv "$target/$build_type/Makefile.builds" builds/Makefile
+
+echo Creating builds/current...
+(echo "# This is the most-recently-configured CVC4 build"; \
+ echo "# 'make' in the top-level source directory applies to this build"; \
+ echo "CURRENT_BUILD = $target/$build_type") > builds/current
+
+for dir in src test; do
+  echo Linking builds/$dir...
+  rm -f "builds/$dir"
+  ln -sfv "$target/$build_type/$dir" "builds/$dir"
+done
+
diff --git a/configure b/configure
index 5c6eead32..15131cbb7 100755
--- a/configure
+++ b/configure
@@ -709,6 +709,7 @@ ac_subst_vars='am__EXEEXT_FALSE
 am__EXEEXT_TRUE
 LTLIBOBJS
 LIBOBJS
+mk_include
 CVC4_PARSER_LIBRARY_VERSION
 CVC4_LIBRARY_VERSION
 CVC4_LIBRARY_RELEASE_CODE
@@ -889,14 +890,13 @@ do
   case $ac_option in
     -*|*=*) ;;
     *) ac_cvc4_build_profile_set=yes
-       $as_echo "$as_me: WARNING: building profile $ac_option" >&2
+       $as_echo "$as_me: CVC4: building profile $ac_option" >&6
        ac_option="--with-build=$ac_option" ;;
   esac
   eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"$ac_option\""'
 done
 eval set x $ac_cvc4_rewritten_args
 shift
-echo "args are now:" "${@}"
 
 # Initialize some variables set by options.
 ac_init_help=
@@ -2793,54 +2793,54 @@ if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "
 else
   non_standard_build_profile=yes
 fi
-build_type_suffix=
+btargs=
 if test -n "${enable_optimized+set}"; then
-  if test "$enable_optimized" = no; then
-    build_type_suffix=$build_type_suffix-noopt
+  if test "$enable_optimized" = yes; then
+    btargs="$btargs opt"
   else
-    build_type_suffix=$build_type_suffix-opt
+    btargs="$btargs noopt"
   fi
 fi
 if test -n "${enable_debug_symbols+set}"; then
-  if test "$enable_debug_symbols" = no; then
-    build_type_suffix=$build_type_suffix-nodsy
+  if test "$enable_debug_symbols" = yes; then
+    btargs="$btargs dsy"
   else
-    build_type_suffix=$build_type_suffix-dsy
+    btargs="$btargs nodsy"
   fi
 fi
 if test -n "${enable_assertions+set}"; then
-  if test "$enable_assertions" = no; then
-    build_type_suffix=$build_type_suffix-noass
+  if test "$enable_assertions" = yes; then
+    btargs="$btargs ass"
   else
-    build_type_suffix=$build_type_suffix-ass
+    btargs="$btargs noass"
   fi
 fi
 if test -n "${enable_tracing+set}"; then
-  if test "$enable_tracing" = no; then
-    build_type_suffix=$build_type_suffix-notrc
+  if test "$enable_tracing" = yes; then
+    btargs="$btargs trc"
   else
-    build_type_suffix=$build_type_suffix-trc
+    btargs="$btargs notrc"
   fi
 fi
 if test -n "${enable_muzzle+set}"; then
-  if test "$enable_muzzle" = no; then
-    build_type_suffix=$build_type_suffix-nomzl
+  if test "$enable_muzzle" = yes; then
+    btargs="$btargs mzl"
   else
-    build_type_suffix=$build_type_suffix-mzl
+    btargs="$btargs nomzl"
   fi
 fi
 if test -n "${enable_coverage+set}"; then
-  if test "$enable_coverage" = no; then
-    build_type_suffix=$build_type_suffix-nocvg
+  if test "$enable_coverage" = yes; then
+    btargs="$btargs cvg"
   else
-    build_type_suffix=$build_type_suffix-cvg
+    btargs="$btargs nocvg"
   fi
 fi
 if test -n "${enable_profiling+set}"; then
-  if test "$enable_profiling" = no; then
-    build_type_suffix=$build_type_suffix-noprf
+  if test "$enable_profiling" = yes; then
+    btargs="$btargs prf"
   else
-    build_type_suffix=$build_type_suffix-prf
+    btargs="$btargs noprf"
   fi
 fi
 { $as_echo "$as_me:${as_lineno-$LINENO}: result: $with_build" >&5
@@ -2848,10 +2848,10 @@ $as_echo "$with_build" >&6; }
 
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for appropriate build string" >&5
 $as_echo_n "checking for appropriate build string... " >&6; }
-build_type=$with_build$build_type_suffix
+build_type=`$ac_confdir/config/build-type $with_build $btargs`
 if test "$non_standard_build_profile" = yes; then
   if test "$with_build" = default; then
-    build_type=custom$build_type_suffix
+    build_type=`$ac_confdir/config/build-type custom $btargs`
   fi
 fi
 { $as_echo "$as_me:${as_lineno-$LINENO}: result: $build_type" >&5
@@ -2867,20 +2867,13 @@ elif test -e src/include/cvc4_config.h; then
   { $as_echo "$as_me:${as_lineno-$LINENO}: result: builds/$target/$build_type" >&5
 $as_echo "builds/$target/$build_type" >&6; }
   echo
-  echo Setting up "builds/$target/$build_type"...
-  rm -fv config.log config.status confdefs.h
-  mkdir -pv "builds/$target/$build_type"
-  ln -sfv "$target/$build_type/Makefile.builds" builds/Makefile
-  echo Creating builds/current...
-  (echo "# This is the most-recently-configured CVC4 build"; \
-   echo "# 'make' in the top-level source directory applies to this build"; \
-   echo "CURRENT_BUILD = $target/$build_type") > builds/current
-  echo Linking builds/src...
-  rm -f builds/src
-  ln -sfv "$target/$build_type/src" builds/src
-  echo Linking builds/test...
-  rm -f builds/test
-  ln -sfv "$target/$build_type/test" builds/test
+  if test -z "$ac_srcdir"; then
+    mkbuilddir=./config/mkbuilddir
+  else
+    mkbuilddir=$ac_srcdir/config/mkbuilddir
+  fi
+  echo $mkbuilddir "$target" "$build_type"
+  $mkbuilddir "$target" "$build_type"
   echo cd "builds/$target/$build_type"
   cd "builds/$target/$build_type"
   CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
@@ -5411,13 +5404,13 @@ if test "${lt_cv_nm_interface+set}" = set; then :
 else
   lt_cv_nm_interface="BSD nm"
   echo "int some_variable = 0;" > conftest.$ac_ext
-  (eval echo "\"\$as_me:5414: $ac_compile\"" >&5)
+  (eval echo "\"\$as_me:5407: $ac_compile\"" >&5)
   (eval "$ac_compile" 2>conftest.err)
   cat conftest.err >&5
-  (eval echo "\"\$as_me:5417: $NM \\\"conftest.$ac_objext\\\"\"" >&5)
+  (eval echo "\"\$as_me:5410: $NM \\\"conftest.$ac_objext\\\"\"" >&5)
   (eval "$NM \"conftest.$ac_objext\"" 2>conftest.err > conftest.out)
   cat conftest.err >&5
-  (eval echo "\"\$as_me:5420: output\"" >&5)
+  (eval echo "\"\$as_me:5413: output\"" >&5)
   cat conftest.out >&5
   if $GREP 'External.*some_variable' conftest.out > /dev/null; then
     lt_cv_nm_interface="MS dumpbin"
@@ -6620,7 +6613,7 @@ ia64-*-hpux*)
   ;;
 *-*-irix6*)
   # Find out which ABI we are using.
-  echo '#line 6623 "configure"' > conftest.$ac_ext
+  echo '#line 6616 "configure"' > conftest.$ac_ext
   if { { eval echo "\"\$as_me\":${as_lineno-$LINENO}: \"$ac_compile\""; } >&5
   (eval $ac_compile) 2>&5
   ac_status=$?
@@ -8088,11 +8081,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:8091: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:8084: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>conftest.err)
    ac_status=$?
    cat conftest.err >&5
-   echo "$as_me:8095: \$? = $ac_status" >&5
+   echo "$as_me:8088: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s "$ac_outfile"; then
      # The compiler can only warn and ignore the option if not recognized
      # So say no if there are warnings other than the usual output.
@@ -8427,11 +8420,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:8430: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:8423: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>conftest.err)
    ac_status=$?
    cat conftest.err >&5
-   echo "$as_me:8434: \$? = $ac_status" >&5
+   echo "$as_me:8427: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s "$ac_outfile"; then
      # The compiler can only warn and ignore the option if not recognized
      # So say no if there are warnings other than the usual output.
@@ -8532,11 +8525,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:8535: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:8528: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>out/conftest.err)
    ac_status=$?
    cat out/conftest.err >&5
-   echo "$as_me:8539: \$? = $ac_status" >&5
+   echo "$as_me:8532: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s out/conftest2.$ac_objext
    then
      # The compiler can only warn and ignore the option if not recognized
@@ -8587,11 +8580,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:8590: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:8583: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>out/conftest.err)
    ac_status=$?
    cat out/conftest.err >&5
-   echo "$as_me:8594: \$? = $ac_status" >&5
+   echo "$as_me:8587: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s out/conftest2.$ac_objext
    then
      # The compiler can only warn and ignore the option if not recognized
@@ -10970,7 +10963,7 @@ else
   lt_dlunknown=0; lt_dlno_uscore=1; lt_dlneed_uscore=2
   lt_status=$lt_dlunknown
   cat > conftest.$ac_ext <<_LT_EOF
-#line 10973 "configure"
+#line 10966 "configure"
 #include "confdefs.h"
 
 #if HAVE_DLFCN_H
@@ -11066,7 +11059,7 @@ else
   lt_dlunknown=0; lt_dlno_uscore=1; lt_dlneed_uscore=2
   lt_status=$lt_dlunknown
   cat > conftest.$ac_ext <<_LT_EOF
-#line 11069 "configure"
+#line 11062 "configure"
 #include "confdefs.h"
 
 #if HAVE_DLFCN_H
@@ -14622,11 +14615,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:14625: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:14618: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>conftest.err)
    ac_status=$?
    cat conftest.err >&5
-   echo "$as_me:14629: \$? = $ac_status" >&5
+   echo "$as_me:14622: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s "$ac_outfile"; then
      # The compiler can only warn and ignore the option if not recognized
      # So say no if there are warnings other than the usual output.
@@ -14721,11 +14714,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:14724: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:14717: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>out/conftest.err)
    ac_status=$?
    cat out/conftest.err >&5
-   echo "$as_me:14728: \$? = $ac_status" >&5
+   echo "$as_me:14721: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s out/conftest2.$ac_objext
    then
      # The compiler can only warn and ignore the option if not recognized
@@ -14773,11 +14766,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:14776: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:14769: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>out/conftest.err)
    ac_status=$?
    cat out/conftest.err >&5
-   echo "$as_me:14780: \$? = $ac_status" >&5
+   echo "$as_me:14773: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s out/conftest2.$ac_objext
    then
      # The compiler can only warn and ignore the option if not recognized
@@ -16359,6 +16352,9 @@ if test "$user_ldflags" = no; then
   LDFLAGS="$CVC4LDFLAGS"
 fi
 
+mk_include=include
+
+
 ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/Makefile src/expr/Makefile src/smt/Makefile src/main/Makefile src/prop/minisat/Makefile src/prop/Makefile src/util/Makefile src/context/Makefile src/parser/Makefile src/parser/cvc/Makefile src/parser/smt/Makefile src/theory/Makefile src/theory/uf/Makefile test/Makefile test/regress/Makefile test/unit/Makefile"
 
 
diff --git a/configure.ac b/configure.ac
index 524f015d8..0b8f8a5f3 100644
--- a/configure.ac
+++ b/configure.ac
@@ -36,63 +36,63 @@ if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "
 else
   non_standard_build_profile=yes
 fi
-build_type_suffix=
+btargs=
 if test -n "${enable_optimized+set}"; then
-  if test "$enable_optimized" = no; then
-    build_type_suffix=$build_type_suffix-noopt
+  if test "$enable_optimized" = yes; then
+    btargs="$btargs opt"
   else
-    build_type_suffix=$build_type_suffix-opt
+    btargs="$btargs noopt"
   fi
 fi
 if test -n "${enable_debug_symbols+set}"; then
-  if test "$enable_debug_symbols" = no; then
-    build_type_suffix=$build_type_suffix-nodsy
+  if test "$enable_debug_symbols" = yes; then
+    btargs="$btargs dsy"
   else
-    build_type_suffix=$build_type_suffix-dsy
+    btargs="$btargs nodsy"
   fi
 fi
 if test -n "${enable_assertions+set}"; then
-  if test "$enable_assertions" = no; then
-    build_type_suffix=$build_type_suffix-noass
+  if test "$enable_assertions" = yes; then
+    btargs="$btargs ass"
   else
-    build_type_suffix=$build_type_suffix-ass
+    btargs="$btargs noass"
   fi
 fi
 if test -n "${enable_tracing+set}"; then
-  if test "$enable_tracing" = no; then
-    build_type_suffix=$build_type_suffix-notrc
+  if test "$enable_tracing" = yes; then
+    btargs="$btargs trc"
   else
-    build_type_suffix=$build_type_suffix-trc
+    btargs="$btargs notrc"
   fi
 fi
 if test -n "${enable_muzzle+set}"; then
-  if test "$enable_muzzle" = no; then
-    build_type_suffix=$build_type_suffix-nomzl
+  if test "$enable_muzzle" = yes; then
+    btargs="$btargs mzl"
   else
-    build_type_suffix=$build_type_suffix-mzl
+    btargs="$btargs nomzl"
   fi
 fi
 if test -n "${enable_coverage+set}"; then
-  if test "$enable_coverage" = no; then
-    build_type_suffix=$build_type_suffix-nocvg
+  if test "$enable_coverage" = yes; then
+    btargs="$btargs cvg"
   else
-    build_type_suffix=$build_type_suffix-cvg
+    btargs="$btargs nocvg"
   fi
 fi
 if test -n "${enable_profiling+set}"; then
-  if test "$enable_profiling" = no; then
-    build_type_suffix=$build_type_suffix-noprf
+  if test "$enable_profiling" = yes; then
+    btargs="$btargs prf"
   else
-    build_type_suffix=$build_type_suffix-prf
+    btargs="$btargs noprf"
   fi
 fi
 AC_MSG_RESULT([$with_build])
 
 AC_MSG_CHECKING([for appropriate build string])
-build_type=$with_build$build_type_suffix
+build_type=`$ac_confdir/config/build-type $with_build $btargs`
 if test "$non_standard_build_profile" = yes; then
   if test "$with_build" = default; then
-    build_type=custom$build_type_suffix
+    build_type=`$ac_confdir/config/build-type custom $btargs`
   fi
 fi
 AC_MSG_RESULT($build_type)
@@ -104,20 +104,13 @@ if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
 elif test -e src/include/cvc4_config.h; then
   AC_MSG_RESULT([builds/$target/$build_type])
   echo
-  echo Setting up "builds/$target/$build_type"...
-  rm -fv config.log config.status confdefs.h
-  mkdir -pv "builds/$target/$build_type"
-  ln -sfv "$target/$build_type/Makefile.builds" builds/Makefile
-  echo Creating builds/current...
-  (echo "# This is the most-recently-configured CVC4 build"; \
-   echo "# 'make' in the top-level source directory applies to this build"; \
-   echo "CURRENT_BUILD = $target/$build_type") > builds/current
-  echo Linking builds/src...
-  rm -f builds/src
-  ln -sfv "$target/$build_type/src" builds/src
-  echo Linking builds/test...
-  rm -f builds/test
-  ln -sfv "$target/$build_type/test" builds/test
+  if test -z "$ac_srcdir"; then
+    mkbuilddir=./config/mkbuilddir
+  else
+    mkbuilddir=$ac_srcdir/config/mkbuilddir
+  fi
+  echo $mkbuilddir "$target" "$build_type"
+  $mkbuilddir "$target" "$build_type"
   echo cd "builds/$target/$build_type"
   cd "builds/$target/$build_type"
   CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
@@ -341,6 +334,9 @@ if test "$user_ldflags" = no; then
   LDFLAGS="$CVC4LDFLAGS"
 fi
 
+mk_include=include
+AC_SUBST(mk_include)
+
 AC_CONFIG_FILES([
   Makefile.builds
   Makefile
diff --git a/contrib/Makefile.in b/contrib/Makefile.in
index e4bf7b362..a86658b70 100644
--- a/contrib/Makefile.in
+++ b/contrib/Makefile.in
@@ -169,6 +169,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/doc/Makefile.in b/doc/Makefile.in
index d5264caff..99ff59b1c 100644
--- a/doc/Makefile.in
+++ b/doc/Makefile.in
@@ -169,6 +169,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/Makefile.in b/src/Makefile.in
index 38d59d02a..de268af16 100644
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -253,6 +253,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/context/Makefile.in b/src/context/Makefile.in
index 51069583d..c4f82d42a 100644
--- a/src/context/Makefile.in
+++ b/src/context/Makefile.in
@@ -198,6 +198,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in
index c7d99dc84..4892220d8 100644
--- a/src/expr/Makefile.in
+++ b/src/expr/Makefile.in
@@ -199,6 +199,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/main/Makefile.in b/src/main/Makefile.in
index 26ea81859..58eeeacdd 100644
--- a/src/main/Makefile.in
+++ b/src/main/Makefile.in
@@ -200,6 +200,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/parser/Makefile.in b/src/parser/Makefile.in
index 859329834..f1b430add 100644
--- a/src/parser/Makefile.in
+++ b/src/parser/Makefile.in
@@ -262,6 +262,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in
index 57db98f0b..3fd1701c8 100644
--- a/src/parser/cvc/Makefile.in
+++ b/src/parser/cvc/Makefile.in
@@ -202,6 +202,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in
index 2e9350486..721ff0e2b 100644
--- a/src/parser/smt/Makefile.in
+++ b/src/parser/smt/Makefile.in
@@ -202,6 +202,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/prop/Makefile.in b/src/prop/Makefile.in
index 311d3f8c7..c6538df38 100644
--- a/src/prop/Makefile.in
+++ b/src/prop/Makefile.in
@@ -236,6 +236,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/prop/minisat/Makefile.in b/src/prop/minisat/Makefile.in
index a54518c74..1dbc8da9f 100644
--- a/src/prop/minisat/Makefile.in
+++ b/src/prop/minisat/Makefile.in
@@ -198,6 +198,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/smt/Makefile.in b/src/smt/Makefile.in
index 9647e51b9..35126e382 100644
--- a/src/smt/Makefile.in
+++ b/src/smt/Makefile.in
@@ -198,6 +198,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/theory/Makefile.in b/src/theory/Makefile.in
index d37387741..dafd68b6c 100644
--- a/src/theory/Makefile.in
+++ b/src/theory/Makefile.in
@@ -236,6 +236,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/theory/uf/Makefile.in b/src/theory/uf/Makefile.in
index dfb8ea932..3b3cd6bbb 100644
--- a/src/theory/uf/Makefile.in
+++ b/src/theory/uf/Makefile.in
@@ -184,6 +184,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/src/util/Makefile.in b/src/util/Makefile.in
index 5627e01a9..3ac892aba 100644
--- a/src/util/Makefile.in
+++ b/src/util/Makefile.in
@@ -199,6 +199,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/test/Makefile.in b/test/Makefile.in
index 69e05dd65..211ec123c 100644
--- a/test/Makefile.in
+++ b/test/Makefile.in
@@ -209,6 +209,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/test/regress/Makefile.in b/test/regress/Makefile.in
index 14c032220..34323b09c 100644
--- a/test/regress/Makefile.in
+++ b/test/regress/Makefile.in
@@ -171,6 +171,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@
diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in
index b630f7765..0b4b68c40 100644
--- a/test/unit/Makefile.in
+++ b/test/unit/Makefile.in
@@ -216,6 +216,7 @@ localedir = @localedir@
 localstatedir = @localstatedir@
 lt_ECHO = @lt_ECHO@
 mandir = @mandir@
+mk_include = @mk_include@
 mkdir_p = @mkdir_p@
 oldincludedir = @oldincludedir@
 pdfdir = @pdfdir@