Makefile

   1 # -*-makefile-*-
   2 #
   3 # This makefile is the _source_ directory's makefile, and is static,
   4 # not generated.  Makefile.am is the automake makefile for the build
   5 # top-level (its corresponding Makefile.in is here, too, but the
   6 # corresponding Makefile is under builds/$arch/$buildid.
   7 #
   8 builddir = builds
   9
  10 .PHONY: all install
  11 all install .DEFAULT:
  12         @if test -d $(builddir); then \
  13                 echo cd $(builddir); \
  14                 cd $(builddir); \
  15                 echo $(MAKE) $@; \
  16                 $(MAKE) $@ || exit 1; \
  17         else \
  18                 echo; \
  19                 echo 'Run configure first, or type "make" in a configured build directory.'; \
  20                 echo; \
  21         fi
  22
  23 distclean maintainerclean:
  24         @if test -d $(builddir); then \
  25                 echo cd $(builddir); \
  26                 cd $(builddir); \
  27                 echo $(MAKE) $@; \
  28                 $(MAKE) $@ || exit 1; \
  29         fi
  30         test -z "$(builddir)" || rm -fr "$(builddir)"
  31         rm -f config.reconfig
  32
  33 # synonyms for "check"
  34 .PHONY: test
  35 test: check
  36
  37 .PHONY: doc doc-internals
  38 doc: doc-builds
  39 doc-internals: doc-internals-builds
  40
  41 .PHONY: examples
  42 examples: all
  43         (cd examples && $(MAKE) $(AM_MAKEFLAGS))
  44
  45 .PHONY: install-examples
  46 install-examples:
  47         (cd examples && $(MAKE) $(AM_MAKEFLAGS) install-data)
  48
  49 YEAR := $(shell date +%Y)
  50 submission submission-main:
  51         @if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \
  52           echo 'ERROR:' >&2; \
  53           echo 'ERROR: Please make maintainer-clean first.' >&2; \
  54           echo 'ERROR:' >&2; \
  55           exit 1; \
  56         fi
  57         ./autogen.sh
  58         ./configure competition --disable-shared --enable-static-binary --with-cln --without-cudd
  59         $(MAKE)
  60         strip builds/bin/cvc4
  61         $(MAKE) check
  62         $(MAKE) -C test/regress/regress1 check
  63         # main track
  64         mkdir -p cvc4-smtcomp-$(YEAR)
  65         cp -p builds/bin/cvc4 cvc4-smtcomp-$(YEAR)/cvc4
  66         cp contrib/run-script-smtcomp2012 cvc4-smtcomp-$(YEAR)/run
  67         chmod 755 cvc4-smtcomp-$(YEAR)/run
  68         tar cf cvc4-smtcomp-$(YEAR).tar cvc4-smtcomp-$(YEAR)
  69 submission-application:
  70         # application track is a separate build because it has different preprocessor #defines
  71         @if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \
  72           echo 'ERROR:' >&2; \
  73           echo 'ERROR: Please make maintainer-clean first.' >&2; \
  74           echo 'ERROR:' >&2; \
  75           exit 1; \
  76         fi
  77         ./autogen.sh
  78         ./configure competition --disable-shared --enable-static-binary --with-cln --without-cudd CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK
  79         $(MAKE)
  80         strip builds/bin/cvc4
  81         $(MAKE) check
  82         $(MAKE) -C test/regress/regress1 check
  83         # package the application track tarball
  84         mkdir -p cvc4-application-smtcomp-$(YEAR)
  85         cp -p builds/bin/cvc4 cvc4-application-smtcomp-$(YEAR)/cvc4
  86         ( echo '#!/bin/sh'; \
  87           echo 'exec ./cvc4 -L smt2 --no-checking --no-interactive --incremental' ) > cvc4-application-smtcomp-$(YEAR)/run
  88         chmod 755 cvc4-application-smtcomp-$(YEAR)/run
  89         tar cf cvc4-application-smtcomp-$(YEAR).tar cvc4-application-smtcomp-$(YEAR)
  90 submission-parallel:
  91         # parallel track can't be built with -cln, so it's a separate build
  92         @if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \
  93           echo 'ERROR:' >&2; \
  94           echo 'ERROR: Please make maintainer-clean first.' >&2; \
  95           echo 'ERROR:' >&2; \
  96           exit 1; \
  97         fi
  98         ./autogen.sh
  99         ./configure competition --disable-shared --enable-static-binary --with-gmp --without-cudd --with-portfolio
 100         $(MAKE)
 101         strip builds/bin/pcvc4
 102         # some test cases fail (and are known to fail)
 103         -$(MAKE) check BINARY=pcvc4
 104         $(MAKE) -C test/regress/regress1 check BINARY=pcvc4
 105         # package the parallel track tarball
 106         mkdir -p cvc4-parallel-smtcomp-$(YEAR)
 107         cp -p builds/bin/pcvc4 cvc4-parallel-smtcomp-$(YEAR)/pcvc4
 108         ( echo '#!/bin/sh'; \
 109           echo 'exec ./pcvc4 --threads 2 -L smt2 --no-checking --no-interactive' ) > cvc4-parallel-smtcomp-$(YEAR)/run
 110         chmod 755 cvc4-parallel-smtcomp-$(YEAR)/run
 111         tar cf cvc4-parallel-smtcomp-$(YEAR).tar cvc4-parallel-smtcomp-$(YEAR)