From 73fd355fd1a9f6cacfc3170d29e29fccc94ab539 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 17 Dec 2009 00:02:12 +0000 Subject: [PATCH] support nonstandard, unconfigured builds (e.g., "./configure debug" followed by "make production ASSERTIONS=1") --- Makefile.am | 15 +++-- Makefile.in | 15 +++-- Makefile.reconf_args | 77 +++++++++++++++++++++++ config/build-type | 59 ++++++++++++++++++ config/cvc4.m4 | 2 +- config/mkbuilddir | 39 ++++++++++++ configure | 116 +++++++++++++++++------------------ configure.ac | 72 ++++++++++------------ contrib/Makefile.in | 1 + doc/Makefile.in | 1 + src/Makefile.in | 1 + src/context/Makefile.in | 1 + src/expr/Makefile.in | 1 + src/main/Makefile.in | 1 + src/parser/Makefile.in | 1 + src/parser/cvc/Makefile.in | 1 + src/parser/smt/Makefile.in | 1 + src/prop/Makefile.in | 1 + src/prop/minisat/Makefile.in | 1 + src/smt/Makefile.in | 1 + src/theory/Makefile.in | 1 + src/theory/uf/Makefile.in | 1 + src/util/Makefile.in | 1 + test/Makefile.in | 1 + test/regress/Makefile.in | 1 + test/unit/Makefile.in | 1 + 26 files changed, 306 insertions(+), 107 deletions(-) create mode 100644 Makefile.reconf_args create mode 100755 config/build-type create mode 100644 config/mkbuilddir 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 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 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 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@ -- 2.30.2