diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /contrib | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'contrib')
-rwxr-xr-x | contrib/build-cudd-with-libtool.sh | 417 | ||||
-rwxr-xr-x | contrib/cut-release | 186 | ||||
-rwxr-xr-x | contrib/update-copyright.pl | 12 |
3 files changed, 615 insertions, 0 deletions
diff --git a/contrib/build-cudd-with-libtool.sh b/contrib/build-cudd-with-libtool.sh new file mode 100755 index 000000000..f291272b2 --- /dev/null +++ b/contrib/build-cudd-with-libtool.sh @@ -0,0 +1,417 @@ +#!/bin/bash +# +# Patch to cudd build system to build everything with libtool, supporting +# shared libraries. Also all libraries are combined into a single one. +# +# This script applies the patch, builds cudd, and, assuming there are no +# errors, reverses the patch. +# +# -- Morgan Deters <mdeters@cs.nyu.edu> Wed, 13 Jul 2011 18:03:11 -0400 +# + +cd "$(dirname "$0")" +if [ $# -ne 1 -o "$1" = -h -o "$1" = -help -o "$1" = --help ]; then + echo "usage: $(basename "$0") cudd-dir" >&2 + exit 1 +fi + +patch="$(pwd)/$(basename "$0")" +if [ ! -r "$patch" ]; then + echo "error: can't read patch at \`$patch'" >&2 + exit 1 +fi +cudd_dir="$1" + +arch=$(../config/config.guess | cut -f1 -d-) +case "$arch" in + i?86) XCFLAGS='-mtune=pentium4 -malign-double -DHAVE_IEEE_754 -DBSD' ;; + x86_64) XCFLAGS='-mtune=native -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8' ;; + *) XCFLAGS= ;; +esac + +set -ex + +XCFLAGS="$XCFLAGS" + +version_info=0:0:0 + +prefix="$cudd_dir" +eprefix="$prefix" +bindir="$eprefix/bin" +datadir="$prefix/share" +includedir="$prefix/include" +libdir="$prefix/lib" +mandir="$datadir/man/man1" +docdir="$datadir/doc" + +cd "$cudd_dir" +patch -p1 < "$patch" +make "XCFLAGS=$XCFLAGS" "CC=libtool --mode=compile gcc" "CPP=libtool --mode=compile g++" libdir="$libdir" version_info="$version_info" DDDEBUG= MTRDEBUG= ICFLAGS=-O2 +mkdir -p "$libdir" +libtool --mode=install cp libcudd.la "$libdir/libcudd.la" +libtool --mode=install cp libcuddxx.la "$libdir/libcuddxx.la" +libtool --mode=install cp libdddmp.la "$libdir/libdddmp.la" +libtool --finish "$libdir" +patch -p1 -R < "$patch" +exit + +# patch follows + +--- a/Makefile ++++ b/Makefile +@@ -221,11 +221,16 @@ + + build: + sh ./setup.sh +- @for dir in $(DIRS); do \ ++ +@for dir in $(BDIRS) obj; do \ + (cd $$dir; \ + echo Making $$dir ...; \ +- make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\ ++ make CC="$(CC)" RANLIB="$(RANLIB)" MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\ + done ++ libtool --mode=link gcc -rpath "$(libdir)" -version-info "$(version_info)" -o libcudd.la cudd/libcudd.la mtr/libmtr.la epd/libepd.la util/libutil.la st/libst.la -lm ++ libtool --mode=link gcc -rpath "${libdir}" -version-info "$(version_info)" -o libdddmp.la dddmp/libdddmp.la ++ libtool --mode=link g++ -rpath "$(libdir)" -version-info "$(version_info)" -o libcuddxx.la obj/libobj.la -lcudd ++ +@(cd nanotrav; \ ++ make CC="$(CC)" RANLIB="$(RANLIB)" MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" ) + + nanotrav: build + +@@ -319,4 +324,6 @@ + echo Cleaning $$dir ...; \ + make -s EXE="$(EXE)" distclean ) \ + done ++ rm -f libcudd* libdddmp* ++ rm -fr .libs + sh ./shutdown.sh +--- a/cudd/Makefile ++++ b/cudd/Makefile +@@ -59,7 +59,7 @@ + cuddZddPort.c cuddZddReord.c cuddZddSetop.c cuddZddSymm.c \ + cuddZddUtil.c + PHDR = cudd.h cuddInt.h +-POBJ = $(PSRC:.c=.o) ++POBJ = $(PSRC:.c=.lo) + PUBJ = $(PSRC:.c=.u) + TARGET = test$(P)$(EXE) + TARGETu = test$(P)-u +@@ -71,12 +71,11 @@ + + #------------------------------------------------------ + +-lib$(P).a: $(POBJ) +- ar rv $@ $? +- $(RANLIB) $@ ++lib$(P).la: $(POBJ) ++ libtool --mode=link gcc -o $@ $? + +-.c.o: $(PSRC) $(PHDR) +- $(CC) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG) ++%.lo: %.c ++ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG) + + optimize_dec: lib$(P).b + +@@ -116,9 +115,10 @@ + programs: $(TARGET) $(TARGETu) lintpgm + + clean: +- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \ ++ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \ + .pure core *.warnings + + distclean: clean +- rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \ ++ rm -f $(TARGET) $(TARGETu) lib*.a lib*.la lib$(P).b llib-l$(P).ln \ + *.bak *~ tags .gdb_history *.qv *.qx ++ rm -fr .libs +--- a/dddmp/Makefile ++++ b/dddmp/Makefile +@@ -148,7 +148,7 @@ + dddmpStoreMisc.c dddmpUtil.c dddmpBinary.c dddmpConvert.c \ + dddmpDbg.c + PHDR = dddmp.h dddmpInt.h $(INCLUDE)/cudd.h $(INCLUDE)/cuddInt.h +-POBJ = $(PSRC:.c=.o) ++POBJ = $(PSRC:.c=.lo) + PUBJ = $(PSRC:.c=.u) + TARGET = test$(P)$(EXE) + TARGETu = test$(P)-u +@@ -182,12 +182,11 @@ + $(WHERE)/mtr/llib-lmtr.ln $(WHERE)/st/llib-lst.ln \ + $(WHERE)/util/llib-lutil.ln + +-lib$(P).a: $(POBJ) +- ar rv $@ $? +- $(RANLIB) $@ ++lib$(P).la: $(POBJ) ++ libtool --mode=link gcc -o $@ $? + +-.c.o: $(PHDR) +- $(CC) -c $< -I$(INCLUDE) $(ICFLAGS) $(XCFLAGS) $(DDDEBUG) $(MTRDEBUG) $(DDDMPDEBUG) $(LDFLAGS) ++%.lo: %.c ++ $(CC) -c -o $@ $< -I$(INCLUDE) $(ICFLAGS) $(XCFLAGS) $(DDDEBUG) $(MTRDEBUG) $(DDDMPDEBUG) $(LDFLAGS) + + optimize_dec: lib$(P).b + +@@ -231,12 +230,13 @@ + #----------------------------------------------------------------------------# + + clean: +- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \ ++ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \ + .pure core *.warnings + + distclean: clean +- rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \ ++ rm -f $(TARGET) $(TARGETu) lib*.a lib*.la lib$(P).b llib-l$(P).ln \ + *.bak *~ tags .gdb_history *.qv *.qx ++ rm -fr .libs + + + +--- a/epd/Makefile ++++ b/epd/Makefile +@@ -19,7 +19,7 @@ + P = epd + PSRC = epd.c + PHDR = epd.h +-POBJ = $(PSRC:.c=.o) ++POBJ = $(PSRC:.c=.lo) + PUBJ = $(PSRC:.c=.u) + + WHERE = .. +@@ -27,12 +27,11 @@ + + #--------------------------- + +-lib$(P).a: $(POBJ) +- ar rv $@ $? +- $(RANLIB) $@ ++lib$(P).la: $(POBJ) ++ libtool --mode=link gcc -o $@ $? + +-.c.o: $(PSRC) $(PHDR) +- $(CC) -c $< -I$(INCLUDE) $(CFLAGS) ++%.lo: %.c ++ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) + + optimize_dec: lib$(P).b + +@@ -58,7 +57,8 @@ + all: lib$(P).a lib$(P).b llib-l$(P).ln tags + + clean: +- rm -f *.o *.u .pure *.warnings ++ rm -f *.o *.lo *.u .pure *.warnings + + distclean: clean +- rm -f lib*.a lib$(P).b llib-l$(P).ln tags *~ *.bak *.qv *.qx ++ rm -f lib*.a lib*.la lib$(P).b llib-l$(P).ln tags *~ *.bak *.qv *.qx ++ rm -fr .libs +--- a/mtr/Makefile ++++ b/mtr/Makefile +@@ -30,7 +30,7 @@ + P = mtr + PSRC = mtrBasic.c mtrGroup.c + PHDR = mtr.h +-POBJ = $(PSRC:.c=.o) ++POBJ = $(PSRC:.c=.lo) + PUBJ = $(PSRC:.c=.u) + SRC = test$(P).c + HDR = +@@ -49,12 +49,11 @@ + + #--------------------------- + +-lib$(P).a: $(POBJ) +- ar rv $@ $? +- $(RANLIB) $@ ++lib$(P).la: $(POBJ) ++ libtool --mode=link gcc -o $@ $? + +-.c.o: $(PSRC) $(PHDR) +- $(CC) -c $< -I$(INCLUDE) $(CFLAGS) $(MTRDEBUG) ++%.lo: %.c ++ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) $(MTRDEBUG) + + optimize_dec: lib$(P).b + +@@ -88,9 +87,10 @@ + cc -O3 $(XCFLAGS) $(LDFLAGS) -o $@ $(UBJ) $(BLIBS) -lm + + clean: +- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \ ++ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \ + .pure core *.warnings + + distclean: clean +- rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \ ++ rm -f $(TARGET) $(TARGETu) lib*.a lib*.la lib$(P).b llib-l$(P).ln \ + *.bak *~ tags *.qv *.qx ++ rm -fr .libs +--- a/nanotrav/Makefile ++++ b/nanotrav/Makefile +@@ -19,9 +19,7 @@ + + INCLUDE = $(WHERE)/include + +-LIBS = $(WHERE)/dddmp/libdddmp.a $(WHERE)/cudd/libcudd.a \ +- $(WHERE)/mtr/libmtr.a $(WHERE)/st/libst.a $(WHERE)/util/libutil.a \ +- $(WHERE)/epd/libepd.a ++LIBS = $(WHERE)/libcudd.la $(WHERE)/libdddmp.la + + MNEMLIB = + #MNEMLIB = $(WHERE)/mnemosyne/libmnem.a +@@ -39,7 +37,7 @@ + HDR = bnet.h ntr.h $(WHERE)/include/dddmp.h $(WHERE)/include/cudd.h \ + $(WHERE)/include/cuddInt.h + +-OBJ = $(SRC:.c=.o) ++OBJ = $(SRC:.c=.lo) + UBJ = $(SRC:.c=.u) + + MFLAG = +@@ -61,10 +59,10 @@ + #------------------------------------------------------ + + $(TARGET): $(SRC) $(OBJ) $(HDR) $(LIBS) $(MNEMLIB) +- $(PURE) $(CC) $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm ++ libtool --mode=link gcc $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm + +-.c.o: $(HDR) +- $(CC) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG) ++%.lo: %.c ++ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG) + + # if the header files change, recompile + $(OBJ): $(HDR) +@@ -91,8 +89,9 @@ + pixie $(TARGETu) + + clean: +- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \ ++ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \ + .pure core *.warnings + + distclean: clean + rm -f $(TARGET) $(TARGETu) *.bak *~ .gdb_history *.qv *.qx ++ rm -fr .libs +--- a/obj/Makefile ++++ b/obj/Makefile +@@ -45,7 +45,7 @@ + P = obj + PSRC = cuddObj.cc + PHDR = cuddObj.hh $(INCLUDE)/cudd.h +-POBJ = $(PSRC:.cc=.o) ++POBJ = $(PSRC:.cc=.lo) + PUBJ = $(PSRC:.cc=.u) + TARGET = test$(P)$(EXE) + TARGETu = test$(P)-u +@@ -57,12 +57,11 @@ + + #------------------------------------------------------ + +-lib$(P).a: $(POBJ) +- ar rv $@ $? +- $(RANLIB) $@ ++lib$(P).la: $(POBJ) ++ libtool --mode=link g++ -o $@ $? + +-.cc.o: $(PHDR) +- $(CPP) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG) ++%.lo: %.cc ++ $(CPP) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG) + + optimize_dec: lib$(P).b + +@@ -102,9 +101,10 @@ + programs: $(TARGET) $(TARGETu) lintpgm + + clean: +- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \ ++ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \ + .pure core *.warnings + + distclean: clean +- rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \ ++ rm -f $(TARGET) $(TARGETu) lib*.a lib*.la lib$(P).b llib-l$(P).ln \ + *.bak *~ tags .gdb_history *.qv *.qx ++ rm -fr .libs +--- a/st/Makefile ++++ b/st/Makefile +@@ -19,7 +19,7 @@ + P = st + PSRC = st.c + PHDR = st.h +-POBJ = $(PSRC:.c=.o) ++POBJ = $(PSRC:.c=.lo) + PUBJ = $(PSRC:.c=.u) + + WHERE = .. +@@ -27,12 +27,11 @@ + + #--------------------------- + +-lib$(P).a: $(POBJ) +- ar rv $@ $? +- $(RANLIB) $@ ++lib$(P).la: $(POBJ) ++ libtool --mode=link gcc -o $@ $? + +-.c.o: $(PHDR) +- $(CC) -c $< -I$(INCLUDE) $(CFLAGS) ++%.lo: %.c ++ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) + + optimize_dec: lib$(P).b + +@@ -58,7 +57,8 @@ + all: lib$(P).a lib$(P).b llib-l$(P).ln tags + + clean: +- rm -f *.o *.u .pure *.warnings ++ rm -f *.o *.lo *.u .pure *.warnings + + distclean: clean +- rm -f lib*.a lib$(P).b llib-l$(P).ln tags *~ *.bak *.qv *.qx ++ rm -f lib*.a lib*.la lib$(P).b llib-l$(P).ln tags *~ *.bak *.qv *.qx ++ rm -fr .libs +--- a/util/Makefile ++++ b/util/Makefile +@@ -21,19 +21,18 @@ + PSRC = cpu_time.c cpu_stats.c getopt.c safe_mem.c strsav.c texpand.c \ + ptime.c prtime.c pipefork.c pathsearch.c stub.c \ + tmpfile.c datalimit.c +-POBJ = $(PSRC:.c=.o) ++POBJ = $(PSRC:.c=.lo) + PUBJ = $(PSRC:.c=.u) + PHDR = util.h + + WHERE = .. + INCLUDE = $(WHERE)/include + +-lib$(P).a: $(POBJ) +- ar rv $@ $? +- $(RANLIB) $@ ++lib$(P).la: $(POBJ) ++ libtool --mode=link gcc -o $@ $? + +-.c.o: $(PHDR) +- $(CC) -c $< -I$(INCLUDE) $(FLAGS) $(CFLAGS) ++%.lo: %.c ++ $(CC) -c -o $@ $< -I$(INCLUDE) $(FLAGS) $(CFLAGS) + + optimize_dec: lib$(P).b + +@@ -59,7 +58,8 @@ + all: lib$(P).a lib$(P).b llib-l$(P).ln tags + + clean: +- rm -f *.o *.u core *.warnings ++ rm -f *.o *.lo *.u core *.warnings + + distclean: clean +- rm -f lib$(P).a lib$(P).b llib-l$(P).ln tags *.bak *~ .pure ++ rm -f lib$(P).a lib$(P).la lib$(P).b llib-l$(P).ln tags *.bak *~ .pure ++ rm -fr .libs diff --git a/contrib/cut-release b/contrib/cut-release new file mode 100755 index 000000000..5ca8d5a9b --- /dev/null +++ b/contrib/cut-release @@ -0,0 +1,186 @@ +#!/bin/bash +# +# usage: cut-release [-n] version-designation [make-args...] +# + +function isthatright { + echo -n "Does that look right? [y/n] " + while read yn; do + if [ "$yn" = y -o "$yn" = Y -o "$yn" = yes -o "$yn" = YES -o "$yn" = Yes ]; then + break + elif [ "$yn" = n -o "$yn" = N -o "$yn" = no -o "$yn" = NO -o "$yn" = No ]; then + echo "Aborting as per user request." >&2 + exit 1 + else + echo -n "[y/n] " + fi + done +} + +if [ "$1" = -n ]; then + dryrun=true + shift +else + dryrun=false +fi + +if [ $# -lt 1 ]; then + echo "Usage: $(basename "$0") [-n] version-designation [make-args...]" >&2 + echo "-n does a dry run (i.e., do sanity checks and build but don't touch the repository)" + exit 1 +fi + +if ! [ -e src/expr/node.h -a -e .svn ]; then + echo "$(basename "$0"): ERROR: you should run this from the top-level of a CVC4 subversion working directory" >&2 + exit 1 +fi + +version="$1" +shift + +if echo "$version" | grep '[^a-zA-Z0-9_.+(){}^%#-]' &>/dev/null; then + echo "$(basename "$0"): ERROR: version designation \`$version' contains illegal characters" >&2 + exit 1 +fi + +vs=($(echo "$version" | sed 's,^\([0-9]*\)\.\([0-9]*\)\(\.\([0-9]*\)\)\?\(.*\),\1 \2 \4 \5,')) +major=${vs[0]} +minor=${vs[1]} +release=${vs[2]-0} +extra=${vs[3]} +echo +echo "Major : $major" +echo "Minor : $minor" +echo "Release: $release" +echo "Extra : $extra" +echo +version="$major.$minor" +if [ "$release" != 0 ]; then + version="$version.$release" +fi +version="$version$extra" +echo "Version: $version" +echo +isthatright + +if ! svn ls "https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version" 2>&1 >/dev/null | grep non-existent >/dev/null; then + echo "$(basename "$0"): ERROR: subversion repo already contains a release \`$version'" >&2 + $dryrun || exit 1 +fi + +if $dryrun; then + if [ -n "$(svn status -q configure.ac)" ]; then + echo "$(basename "$0"): ERROR: in dry-run mode, cannot operate properly with local modifications to \"configure.ac\", sorry" >&2 + exit 1 + fi +elif [ -n "$(svn status -q)" ]; then + echo "$(basename "$0"): ERROR: \"svn status\" indicates there are local modifications; please commit first" >&2 + exit 1 +fi + +root="$(svn info | grep "^Repository Root: https://subversive.cims.nyu.edu/.*" | cut -f3 -d' ')" +if [ -z "$root" ]; then + echo "$(basename "$0"): ERROR: can't get repository root URL" 2>&1 + $dryrun || exit 1 +fi + +if [ `svn -uq status | wc -l` -ne 1 ]; then + echo "$(basename "$0"): ERROR: this working directory isn't up to date" 2>&1 + $dryrun || exit 1 +fi + +if ! grep '^m4_define(_CVC4_MAJOR, *[0-9][0-9]* *)' configure.ac &>/dev/null || + ! grep '^m4_define(_CVC4_MINOR, *[0-9][0-9]* *)' configure.ac &>/dev/null || + ! grep '^m4_define(_CVC4_RELEASE, *[0-9][0-9]* *)' configure.ac &>/dev/null || + ! grep '^m4_define(_CVC4_EXTRAVERSION, *\[.*\] *)' configure.ac &>/dev/null; then + echo "$(basename "$0"): ERROR: cannot locate the version info lines of configure.ac" >&2 + $dryrun || exit 1 +fi +perl -pi -e 's/^m4_define\(_CVC4_MAJOR, ( *)[0-9]+( *)\)/m4_define(_CVC4_MAJOR, ${1}'"$major"'$2)/; + s/^m4_define\(_CVC4_MINOR, ( *)[0-9]+( *)\)/m4_define(_CVC4_MINOR, ${1}'"$minor"'$2)/; + s/^m4_define\(_CVC4_RELEASE, ( *)[0-9]+( *)\)/m4_define(_CVC4_RELEASE, ${1}'"$release"'$2)/; + s/^m4_define\(_CVC4_EXTRAVERSION, ( *)\[.*\]( *)\)/m4_define(_CVC4_EXTRAVERSION, $1\['"$extra"'\]$2)/' configure.ac + +trap 'echo; echo; echo "Aborting in error."; svn revert configure.ac; echo' EXIT + +echo +echo 'Made the following change to configure.ac:' +echo +svn diff configure.ac +echo +isthatright + +if ! grep '^m4_define(_CVC4_MAJOR, *'"$major"' *)' configure.ac &>/dev/null || + ! grep '^m4_define(_CVC4_MINOR, *'"$minor"' *)' configure.ac &>/dev/null || + ! grep '^m4_define(_CVC4_RELEASE, *'"$release"' *)' configure.ac &>/dev/null || + ! grep '^m4_define(_CVC4_EXTRAVERSION, *\['"$extra"'\] *)' configure.ac &>/dev/null; then + echo "$(basename "$0"): INTERNAL ERROR: cannot find the modified version info lines in configure.ac, bailing..." >&2 + exit 1 +fi +if [ -z "$(svn status -q configure.ac)" ]; then + echo "$(basename "$0"): INTERNAL ERROR: \"svn status\" indicates there are no local modifications to configure.ac; I expected the ones I just made!" >&2 + exit 1 +fi + +if ! $SHELL -c '\ + version="'$version'"; \ + set -ex; \ + ./autogen.sh; \ + mkdir "release-$version"; \ + cd "release-$version"; \ + ../configure production-cln-staticbinary --disable-shared --enable-unit-testing --with-cudd --with-readline; \ + make dist "$@"; \ + tar xf "cvc4-$version.tar.gz"; \ + cd "cvc4-$version"; \ + ./configure production-cln-staticbinary --disable-shared --enable-unit-testing --with-cudd --with-readline; \ + make check "$@"; \ + make distcheck "$@"; \ +'; then + exit 1 +fi + +if ! [ -e release-$version/cvc4-$version.tar.gz ]; then + echo "$(basename "$0"): INTERNAL ERROR: cannot find the distribution tarball I just built" >&2 + exit 1 +fi +if ! [ -e release-$version/src/main/cvc4 ]; then + echo "$(basename "$0"): INTERNAL ERROR: cannot find the binary I just built" >&2 + exit 1 +fi + +echo +echo 'This release of CVC4 will identify itself as:' +echo +release-$version/src/main/cvc4 --version +echo +isthatright + +echo +echo 'This binary release of CVC4 will identify itself as being configured like this:' +echo +release-$version/src/main/cvc4 --show-config +echo +isthatright + +echo +echo "Signing tarball..." +cp -p "release-$version/cvc4-$version.tar.gz" . +gpg -b --armor "cvc4-$version.tar.gz" + +echo +echo "Signing binary..." +cp -p "release-$version/src/main/cvc4" "cvc4-$version" +gpg -b --armor "cvc4-$version" + +echo +echo "About to run: svn commit -m \"Cutting release $version.\"" +isthatright +$dryrun || svn commit -m "Cutting release $version." + +echo +echo "About to run: svn copy -m \"Cutting release $version.\" \"$root\" \"https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version\"" +isthatright +$dryrun || svn copy -m "Cutting release $version." "$root" "https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version" + +trap '' EXIT + diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 93ec5e6f0..282bffd5d 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -5,6 +5,7 @@ # Copyright (c) 2009, 2010, 2011 The CVC4 Project # # usage: update-copyright [-m] [files/directories...] +# update-copyright [-h | --help] # # This script goes through a source directory rewriting the top bits of # source files to match a template (inline, below). For files with no @@ -29,6 +30,7 @@ # It ignores any directory matching $excluded_directories # (so, you should add here any sources imported but not covered under # the license.) +# my $excluded_directories = '^(minisat|CVS|generated)$'; # re-include bounded_token_buffer.{h,cpp} @@ -65,6 +67,16 @@ use Fcntl ':mode'; my $dir = $0; $dir =~ s,/[^/]+/*$,,; +if($#ARGV >= 0 && $ARGV[0] eq '-h' || $ARGV[0] eq '--help') { + open(my $SELF, $0) || die "error opening $0 for reading"; + while($_ = <$SELF>) { + last if !/^#/; + print; + } + close $SELF; + exit; +} + # whether we ONLY process files with svn status "M" my $modonly = 0; |