Merge branch '1.4.x'

[cvc5.git] / .travis.yml

diff --git a/.travis.yml b/.travis.yml
index 6d4b4b85242785ad81129f8b9f01576e4e4f542a..18204d3c6923eca209d24eeef863b7ab464c1be8 100644 (file)
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,38 +1,86 @@
 language: cpp
+cache: apt
 compiler:
  - gcc
  - clang
 env:
- - TRAVIS_CVC4_CONFIG='production-cln --enable-language-bindings=java,c'
- - TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c'
- - TRAVIS_CVC4_DISTCHECK=yes
+ - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c'
+ - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c'
+ - TRAVIS_CVC4=yes TRAVIS_CVC4_DISTCHECK=yes
+ - TRAVIS_LFSC=yes
+ - TRAVIS_LFSC=yes TRAVIS_LFSC_DISTCHECK=yes
 before_install:
 # dhart/ppa is for cxxtest package, which doesn't appear officially until quantal
  - travis_retry sudo apt-add-repository -y ppa:dhart/ppa
  - travis_retry sudo apt-get update -qq
- - travis_retry sudo apt-get install -qq libgmp-dev antlr3 libantlr3c-dev libboost-dev libboost-thread-dev swig2.0 libcln-dev cxxtest openjdk-7-jdk
+ - travis_retry sudo apt-get install -qq libgmp-dev antlr3 libantlr3c-dev libboost-dev libboost-thread-dev swig2.0 libcln-dev openjdk-7-jdk
+ - travis_retry sudo apt-get install -qq --force-yes cxxtest
 before_script:
  - export JAVA_HOME=/usr/lib/jvm/java-7-openjdk-amd64
  - export PATH=$PATH:$JAVA_HOME/bin
  - export JAVA_CPPFLAGS=-I$JAVA_HOME/include
  - ./autogen.sh
- - echo $TRAVIS_CVC4_CONFIG
- - normal="$(echo -e '\033[0m')" red="$normal$(echo -e '\033[01;31m')" green="$normal$(echo -e '\033[01;32m')"
- - ./configure --enable-unit-testing --enable-proof --with-portfolio $TRAVIS_CVC4_CONFIG || (echo; cat builds/config.log; echo; echo "${red}CONFIGURE FAILED${normal}"; exit 1)
 script:
- - normal="$(echo -e '\033[0m')" red="$normal$(echo -e '\033[01;31m')" green="$normal$(echo -e '\033[01;32m')"
- - if [ -n "$TRAVIS_CVC4_DISTCHECK" ]; then
-     make -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}DISTCHECK FAILED${normal}"; echo; exit 1);
-   else
-     (make -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}BUILD/TEST FAILED${normal}"; echo; exit 1)) &&
-     (make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' || (echo; echo "${red}PORTFOLIO TEST FAILED${normal}"; echo; exit 1)) &&
-     (make -j2 examples || (echo; echo "${red}COULD NOT BUILD EXAMPLES${normal}"; echo; exit 1));
-   fi &&
-   (echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}")
+ - |
+   echo "travis_fold:start:load_script"
+   normal="$(echo -e '\033[0m')" red="$normal$(echo -e '\033[01;31m')" green="$normal$(echo -e '\033[01;32m')"
+   configureCVC4() {
+     echo "CVC4 config - $TRAVIS_CVC4_CONFIG";
+     ./configure --enable-unit-testing --enable-proof --with-portfolio $TRAVIS_CVC4_CONFIG ||
+       (echo; cat builds/config.log; error "CONFIGURE FAILED");
+   }
+   error() {
+     echo;
+     echo "${red}${1}${normal}";
+     echo;
+     exit 1;
+   }
+   makeDistcheck() {
+     make -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' ||
+       error "DISTCHECK (WITH NEWTHEORY TESTS) FAILED";
+   }
+   makeCheck() {
+     make -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/TEST FAILED";
+   }
+   makeCheckPortfolio() {
+     make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' RUN_REGRESSION_ARGS= ||
+       error "PORTFOLIO TEST FAILED";
+   }
+   makeExamples() {
+     make -j2 examples || error "COULD NOT BUILD EXAMPLES${normal}";
+   }
+   addNewTheoryTest() {
+       contrib/new-theory test_newtheory || error "NEWTHEORY FAILED";
+       grep -q '^THEORIES *=.* test_newtheory' src/Makefile.am || error "NEWTHEORY FAILED";
+       contrib/new-theory --alternate test_newtheory test_newalttheory || error "NEWTHEORY-ALTERNATE FAILED";
+       grep -q '^THEORIES *=.* test_newalttheory' src/Makefile.am || error "NEWTHEORY-ALTERNATE FAILED";
+   }
+   LFSCchecks() {
+     cd proofs/lfsc_checker &&
+     (./configure || (echo; cat builds/config.log; echo; echo "${red}CONFIGURE FAILED${normal}"; exit 1)) &&
+     if [ -n "$TRAVIS_LFSC_DISTCHECK" ]; then
+       make -j2 distcheck || (echo; echo "${red}LFSC DISTCHECK FAILED${normal}"; echo; exit 1);
+     else
+       make -j2 || (echo; echo "${red}LFSC BUILD FAILED${normal}"; echo; exit 1);
+     fi;
+   }
+   run() {
+     echo "travis_fold:start:$1"
+     echo "Running $1"
+     $1 || exit 1
+     echo "travis_fold:end:$1"
+   }
+   [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_DISTCHECK" ] && run addNewTheoryTest
+   [ -n "$TRAVIS_CVC4" ] && run configureCVC4
+   [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_DISTCHECK" ] && run makeDistcheck
+   [ -n "$TRAVIS_CVC4" ] && [ -z "$TRAVIS_CVC4_DISTCHECK" ] && run makeCheck && run makeCheckPortfolio && run makeExamples
+   [ -n "$TRAVIS_LFSC" ] && run LFSCchecks
+   [ -z "$TRAVIS_CVC4" ] && [ -z "$TRAVIS_LFSC" ] && error "Unknown Travis-CI configuration"
+   echo "travis_fold:end:load_script"
+ - echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}"
 matrix:
   fast_finish: true
 notifications:
   email:
-    recipients: mdeters@cs.nyu.edu
     on_success: change
     on_failure: always