blob: 6ef64f0e242209e8c9bd643da3a328e2e229f0d2 (
plain)
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
132
133
134
135
136
137
138
139
140
141
142
143
144
|
language: cpp
cache:
apt: true
directories:
- $HOME/cxxtest
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="
matrix:
- TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c --enable-proof --with-portfolio'
- TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio'
- TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='--disable-proof'
- TRAVIS_CVC4=yes TRAVIS_CVC4_DISTCHECK=yes TRAVIS_CVC4_CONFIG='--enable-proof'
- TRAVIS_LFSC=yes
- TRAVIS_LFSC=yes TRAVIS_LFSC_DISTCHECK=yes
addons:
apt:
sources:
- ubuntu-toolchain-r-test
packages:
- libgmp-dev
- libboost-dev
- libboost-thread-dev
- swig
- libcln-dev
- openjdk-7-jdk
- antlr3
- libantlr3c-dev
install:
# Download and cache a copy of cxxtest until it appears officially in quantal.
- wget http://sourceforge.net/projects/cxxtest/files/cxxtest/4.3/cxxtest-4.3.tar.gz
- tar -xzvf cxxtest-4.3.tar.gz
- cp -vRT cxxtest-4.3 $HOME/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 CXXTEST=$HOME/cxxtest ||
(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' DISTCHECK_CONFIGURE_FLAGS="CXXTEST=$HOME/cxxtest" ||
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";
}
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";
}
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 makeExamples
[ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_CHECK_PORTFOLIO" ] && run makeCheckPortfolio
[ -n "$TRAVIS_LFSC" ] && run LFSCchecks
[ -n "$TRAVIS_COVERITY" ] && echo "Running coverity. Skipping the normal build."
[ -z "$TRAVIS_CVC4" ] && [ -z "$TRAVIS_LFSC" ] && [ -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' CXXTEST="$HOME/cxxtest"
addons:
# Need to duplicate as addons will be over written.
apt:
sources:
- ubuntu-toolchain-r-test
packages:
- libgmp-dev
- libboost-dev
- libboost-thread-dev
- swig
- libcln-dev
- openjdk-7-jdk
- antlr3
- libantlr3c-dev
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
|
