diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 123 |
1 files changed, 82 insertions, 41 deletions
@@ -40,85 +40,126 @@ doc: doc-builds doc-internals: doc-internals-builds YEAR := $(shell date +%Y) -submission submission-main: +submission: + @if [ -d builds-smtcomp ]; then \ + echo 'ERROR: remove the builds-smtcomp directory' >&2; \ + exit 1; \ + fi + @if test -d cvc4-smtcomp-$(YEAR) || test -e cvc4-smtcomp-$(YEAR).zip || \ + test -d cvc4-smtcomp-main-$(YEAR) || test -e cvc4-smtcomp-main-$(YEAR).zip || \ + test -d cvc4-smtcomp-application-$(YEAR) || test -e cvc4-smtcomp-application-$(YEAR).zip || \ + test -d cvc4-smtcomp-parallel-$(YEAR) || test -e cvc4-smtcomp-parallel-$(YEAR).zip; then \ + echo 'ERROR: remove cvc4-smtcomp*-$(YEAR) and corresponding zipfiles.' >&2; \ + exit 1; \ + fi + $(MAKE) submission-main + $(MAKE) submission-application + $(MAKE) submission-parallel + mkdir -p cvc4-smtcomp-$(YEAR)/bin + cp -p cvc4-smtcomp-main-$(YEAR)/bin/cvc4 cvc4-smtcomp-$(YEAR)/bin/cvc4-main + cp -p cvc4-smtcomp-main-$(YEAR)/bin/starexec_run_default cvc4-smtcomp-$(YEAR)/bin/starexec_run_default + cp -p cvc4-smtcomp-application-$(YEAR)/bin/cvc4 cvc4-smtcomp-$(YEAR)/bin/cvc4-application + cp -p cvc4-smtcomp-application-$(YEAR)/bin/starexec_run_default cvc4-smtcomp-$(YEAR)/bin/starexec_run_application + cp -p cvc4-smtcomp-parallel-$(YEAR)/bin/cvc4 cvc4-smtcomp-$(YEAR)/bin/pcvc4 + cp -p cvc4-smtcomp-parallel-$(YEAR)/bin/starexec_run_default cvc4-smtcomp-$(YEAR)/bin/starexec_run_parallel + cat cvc4-smtcomp-main-$(YEAR)/starexec_description.txt \ + cvc4-smtcomp-application-$(YEAR)/starexec_description.txt \ + cvc4-smtcomp-parallel-$(YEAR)/starexec_description.txt \ + > cvc4-smtcomp-$(YEAR)/starexec_description.txt + cd cvc4-smtcomp-$(YEAR) && zip -r ../cvc4-smtcomp-$(YEAR).zip * +submission-main: + @if [ -d builds-smtcomp/main ]; then \ + echo 'ERROR: remove the builds-smtcomp/main directory' >&2; \ + exit 1; \ + fi @if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \ echo 'ERROR:' >&2; \ echo 'ERROR: Please make maintainer-clean first.' >&2; \ echo 'ERROR:' >&2; \ exit 1; \ fi - @if test -d cvc4-smtcomp-$(YEAR) || test -e cvc4-smtcomp-$(YEAR).zip; then \ + @if test -d cvc4-smtcomp-main-$(YEAR) || test -e cvc4-smtcomp-main-$(YEAR).zip; then \ echo 'ERROR:' >&2; \ - echo 'ERROR: Please remove cvc4-smtcomp-$(YEAR) and cvc4-smtcomp-$(YEAR).zip first.' >&2; \ + echo 'ERROR: Please remove cvc4-smtcomp-main-$(YEAR) and cvc4-smtcomp-main-$(YEAR).zip first.' >&2; \ echo 'ERROR:' >&2; \ exit 1; \ fi ./autogen.sh - ./configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl - $(MAKE) - strip builds/bin/cvc4 - $(MAKE) check - #$(MAKE) -C test/regress/regress1 check + mkdir -p builds-smtcomp/main + ( cd builds-smtcomp/main; \ + ../../configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl; \ + $(MAKE) V=1; \ + strip src/main/cvc4; \ + $(MAKE) check ) # main track - mkdir -p cvc4-smtcomp-$(YEAR)/bin - cp -p builds/bin/cvc4 cvc4-smtcomp-$(YEAR)/bin/cvc4 - cp contrib/run-script-smtcomp2014 cvc4-smtcomp-$(YEAR)/bin/starexec_run_default - chmod 755 cvc4-smtcomp-$(YEAR)/bin/starexec_run_default - echo "CVC4 for SMT_COMP main track `builds/bin/cvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-smtcomp-$(YEAR)/starexec_description.txt - cd cvc4-smtcomp-$(YEAR) && zip -r ../cvc4-smtcomp-$(YEAR).zip * + mkdir -p cvc4-smtcomp-main-$(YEAR)/bin + cp -p builds-smtcomp/main/src/main/cvc4 cvc4-smtcomp-main-$(YEAR)/bin/cvc4 + cp contrib/run-script-smtcomp2014 cvc4-smtcomp-main-$(YEAR)/bin/starexec_run_default + chmod 755 cvc4-smtcomp-main-$(YEAR)/bin/starexec_run_default + echo "CVC4 for SMT_COMP main track `builds-smtcomp/main/src/main/cvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-smtcomp-main-$(YEAR)/starexec_description.txt + cd cvc4-smtcomp-main-$(YEAR) && zip -r ../cvc4-smtcomp-main-$(YEAR).zip * submission-application: # application track is a separate build because it has different preprocessor #defines + @if [ -d builds-smtcomp/application ]; then \ + echo 'ERROR: remove the builds-smtcomp/main directory' >&2; \ + exit 1; \ + fi @if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \ echo 'ERROR:' >&2; \ echo 'ERROR: Please make maintainer-clean first.' >&2; \ echo 'ERROR:' >&2; \ exit 1; \ fi - @if test -d cvc4-application-smtcomp-$(YEAR) || test -e cvc4-application-smtcomp-$(YEAR).zip; then \ + @if test -d cvc4-smtcomp-application-$(YEAR) || test -e cvc4-smtcomp-application-$(YEAR).zip; then \ echo 'ERROR:' >&2; \ - echo 'ERROR: Please remove cvc4-application-smtcomp-$(YEAR) and cvc4-application-smtcomp-$(YEAR).zip first.' >&2; \ + echo 'ERROR: Please remove cvc4-smtcomp-application-$(YEAR) and cvc4-smtcomp-application-$(YEAR).zip first.' >&2; \ echo 'ERROR:' >&2; \ exit 1; \ fi ./autogen.sh - ./configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK - $(MAKE) - strip builds/bin/cvc4 - $(MAKE) check - #$(MAKE) -C test/regress/regress1 check + mkdir -p builds-smtcomp/application + ( cd builds-smtcomp/application; \ + ../../configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK; \ + $(MAKE) V=1; \ + strip src/main/cvc4; \ + $(MAKE) check ) # package the application track zipfile - mkdir -p cvc4-application-smtcomp-$(YEAR)/bin - cp -p builds/bin/cvc4 cvc4-application-smtcomp-$(YEAR)/bin/cvc4 - cp contrib/run-script-smtcomp2014-application cvc4-application-smtcomp-$(YEAR)/bin/starexec_run_default - chmod 755 cvc4-application-smtcomp-$(YEAR)/bin/starexec_run_default - echo "CVC4 for SMT_COMP application track `builds/bin/cvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-application-smtcomp-$(YEAR)/starexec_description.txt - cd cvc4-application-smtcomp-$(YEAR) && zip -r ../cvc4-application-smtcomp-$(YEAR).zip * + mkdir -p cvc4-smtcomp-application-$(YEAR)/bin + cp -p builds-smtcomp/application/src/main/cvc4 cvc4-smtcomp-application-$(YEAR)/bin/cvc4 + cp contrib/run-script-smtcomp2014-application cvc4-smtcomp-application-$(YEAR)/bin/starexec_run_default + chmod 755 cvc4-smtcomp-application-$(YEAR)/bin/starexec_run_default + echo "CVC4 for SMT_COMP application track `builds-smtcomp/application/src/main/cvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-smtcomp-application-$(YEAR)/starexec_description.txt + cd cvc4-smtcomp-application-$(YEAR) && zip -r ../cvc4-smtcomp-application-$(YEAR).zip * submission-parallel: # parallel track can't be built with -cln, so it's a separate build + @if [ -d builds-smtcomp/parallel ]; then \ + echo 'ERROR: remove the builds-smtcomp/main directory' >&2; \ + exit 1; \ + fi @if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \ echo 'ERROR:' >&2; \ echo 'ERROR: Please make maintainer-clean first.' >&2; \ echo 'ERROR:' >&2; \ exit 1; \ fi - @if test -d cvc4-parallel-smtcomp-$(YEAR) || test -e cvc4-parallel-smtcomp-$(YEAR).zip; then \ + @if test -d cvc4-smtcomp-parallel-$(YEAR) || test -e cvc4-smtcomp-parallel-$(YEAR).zip; then \ echo 'ERROR:' >&2; \ - echo 'ERROR: Please remove cvc4-parallel-smtcomp-$(YEAR) and cvc4-parallel-smtcomp-$(YEAR).zip first.' >&2; \ + echo 'ERROR: Please remove cvc4-smtcomp-parallel-$(YEAR) and cvc4-smtcomp-parallel-$(YEAR).zip first.' >&2; \ echo 'ERROR:' >&2; \ exit 1; \ fi ./autogen.sh - ./configure competition --disable-shared --enable-static-binary --with-gmp --with-portfolio --with-glpk --with-abc --without-readline --enable-gpl - $(MAKE) - strip builds/bin/pcvc4 - # some test cases fail (and are known to fail) - -$(MAKE) check BINARY=pcvc4 - #$(MAKE) -C test/regress/regress1 check BINARY=pcvc4 + mkdir -p builds-smtcomp/parallel + ( cd builds-smtcomp/parallel; \ + ../../configure competition --disable-shared --enable-static-binary --with-gmp --with-portfolio --with-glpk --with-abc --without-readline --enable-gpl; \ + $(MAKE) V=1; \ + strip src/main/pcvc4; \ + $(MAKE) check BINARY=pcvc4 CVC4_REGRESSION_ARGS=--fallback-sequential ) # package the parallel track zipfile - mkdir -p cvc4-parallel-smtcomp-$(YEAR)/bin - cp -p builds/bin/pcvc4 cvc4-parallel-smtcomp-$(YEAR)/bin/pcvc4 + mkdir -p cvc4-smtcomp-parallel-$(YEAR)/bin + cp -p builds-smtcomp/parallel/src/main/pcvc4 cvc4-smtcomp-parallel-$(YEAR)/bin/pcvc4 ( echo '#!/bin/sh'; \ - echo 'exec ./pcvc4 --threads 2 -L smt2 --no-checking --no-interactive "$@"' ) > cvc4-parallel-smtcomp-$(YEAR)/bin/starexec_run_default - chmod 755 cvc4-parallel-smtcomp-$(YEAR)/bin/starexec_run_default - echo "CVC4 for SMT_COMP parallel track `builds/bin/cvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-parallel-smtcomp-$(YEAR)/starexec_description.txt - cd cvc4-parallel-smtcomp-$(YEAR) && zip -r ../cvc4-parallel-smtcomp-$(YEAR).zip * + echo 'exec ./pcvc4 --threads 2 -L smt2 --no-checking --no-interactive "$@"' ) > cvc4-smtcomp-parallel-$(YEAR)/bin/starexec_run_default + chmod 755 cvc4-smtcomp-parallel-$(YEAR)/bin/starexec_run_default + echo "CVC4 for SMT_COMP parallel track `builds-smtcomp/parallel/src/main/pcvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-smtcomp-parallel-$(YEAR)/starexec_description.txt + cd cvc4-smtcomp-parallel-$(YEAR) && zip -r ../cvc4-smtcomp-parallel-$(YEAR).zip * |