.travis.yml


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131

language: cpp
cache:
 apt: true

sudo: required
dist: trusty

compiler:
 - gcc
 - clang
env:
 global:
  # The next declaration is the encrypted COVERITY_SCAN_TOKEN, created
  #   via the "travis encrypt" command using the project repo's public key
  - secure: "fRfdzYwV10VeW5tVSvy5qpR8ZlkXepR7XWzCulzlHs9SRI2YY20BpzWRjyMBiGu2t7IeJKT7qdjq/CJOQEM8WS76ON7QJ1iymKaRDewDs3OhyPJ71fsFKEGgLky9blk7I9qZh23hnRVECj1oJAVry9IK04bc2zyIEjUYpjRkUAQ="
  - TEST_GROUPS=2
 matrix:
  - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_JAVA_API_TEST=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c --with-lfsc --with-portfolio'
  - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_JAVA_API_TEST=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --with-lfsc --with-portfolio' TEST_GROUP=0
  - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --with-lfsc --with-portfolio' TEST_GROUP=1
  - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='--disable-proof'
  - TRAVIS_CVC4=yes TRAVIS_CVC4_DISTCHECK=yes TRAVIS_CVC4_CONFIG='--enable-proof'
addons:
 apt:
  sources:
  - ubuntu-toolchain-r-test
  packages: &common_deps
  - libgmp-dev
  - libboost-dev
  - libboost-thread-dev
  - swig
  - libcln-dev
  - openjdk-7-jdk
  - antlr3
  - libantlr3c-dev
  - ant-optional
  - 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
script:
 - |
   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 $TRAVIS_CVC4_CONFIG ||
       (echo; echo "Trying to print config.log"; cat builds/config.log; error "CONFIGURE FAILED");
   }
   error() {
     echo;
     echo "${red}${1}${normal}";
     echo;
     exit 1;
   }
   makeDistcheck() {
     make V=1 -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' ||
       error "DISTCHECK (WITH NEWTHEORY TESTS) FAILED";
   }
   makeCheck() {
     make V=1 -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/TEST FAILED";
   }
   makeCheckPortfolio() {
     make V=1 -j2 check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' RUN_REGRESSION_ARGS= ||
       error "PORTFOLIO TEST FAILED";
   }
   JavaApiTest() {
     pushd test/java
     local status=0
     ant || status=1
     popd
     return $status
   }
   makeExamples() {
     make V=1 -j2 examples || error "COULD NOT BUILD EXAMPLES${normal}";
   }
   addNewTheoryTest() {
       contrib/new-theory test_newtheory || error "NEWTHEORY FAILED";
       grep -q '^THEORIES *=.* test_newtheory' src/Makefile.theories || error "NEWTHEORY FAILED";
       contrib/new-theory --alternate test_newtheory test_newalttheory || error "NEWTHEORY-ALTERNATE FAILED";
       grep -q '^THEORIES *=.* test_newalttheory' src/Makefile.theories || error "NEWTHEORY-ALTERNATE FAILED";
   }
   run() {
     echo "travis_fold:start:$1"
     echo "Running $1"
     $1 || exit 1
     echo "travis_fold:end:$1"
   }
   [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_WITH_LFSC" ] && run contrib/get-lfsc-checker
   [ -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 makeExamples
   [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_CHECK_PORTFOLIO" ] && run makeCheckPortfolio
   # [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_JAVA_API_TEST" ] && run JavaApiTest
   [ -n "$TRAVIS_COVERITY" ] && echo "Running coverity. Skipping the normal build."
   [ -z "$TRAVIS_CVC4" ] && [ -z "$TRAVIS_COVERITY" ] && error "Unknown Travis-CI configuration"
   echo "travis_fold:end:load_script"
 - echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}"
matrix:
  fast_finish: true
  # Rule for running Coverity Scan.
  include:
    - os: linux
      compiler: gcc
      before_install: echo -n | openssl s_client -connect scan.coverity.com:443 | sed -ne '/-BEGIN CERTIFICATE-/,/-END CERTIFICATE-/p' | sudo tee -a /etc/ssl/certs/ca-
      env:
        - TRAVIS_COVERITY=yes CVC4_REGRESSION_ARGS='--no-early-exit'
      addons:
        # Need to duplicate as addons will be over written.
        apt:
          sources:
            - ubuntu-toolchain-r-test
          packages:
            - *common_deps
        coverity_scan:
          project:
            name: "CVC4/CVC4"
            description: "Build submitted via Travis CI"
          notification_email: timothy.alan.king@gmail.com
          build_command_prepend: "./autogen.sh; ./configure --enable-unit-testing --enable-proof"
          build_command: "make V=1 -j4"
          branch_pattern: coverity_scan
      after_failure:
        - cat /home/travis/build/CVC4/CVC4/cov-int/build-log.txt
notifications:
  email:
    on_success: change
    on_failure: always