blob: 27cb2915bd279e759571f6fd3990ddd58ecc5391 (
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
145
146
147
148
149
150
151
152
153
154
155
|
# Fix Travis write errors on Clang builds. These write errors occurred after
# a Travis update to new Trusty images on Dec. 12th 2017. The reason for these
# write errors is unknown. Using the deprecated builds did not fix the problem.
# Setting 'filter_secrets: false' as suggested here
# https://github.com/travis-ci/travis-ci/issues/4704#issuecomment-321777557
# fixes the problem.
filter_secrets: false
language: cpp
cache:
- apt
- ccache
# We need more than 4G memory for compiling CVC4. Hence, we cannot switch
# to container-based virtualization environments since they only provide 4G of
# memory. We will stick with the VM-based environments for now.
sudo: required
dist: trusty
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
- CCACHE_COMPRESS=1
addons:
apt:
sources:
- ubuntu-toolchain-r-test
packages: &common_deps
- libgmp-dev
- libboost-dev
- libboost-thread-dev
- swig3.0
- libcln-dev
- openjdk-7-jdk
- antlr3
- libantlr3c-dev
- ant-optional
- cxxtest
- libreadline-dev
before_install:
- eval "${MATRIX_EVAL}"
# Clang does not play nice with ccache (at least the versions offered by
# Travis), use a workaround:
# https://github.com/travis-ci/travis-ci/issues/5383#issuecomment-224630584
- |
if [ "$TRAVIS_OS_NAME" == "linux" ] && [ "$CXX" == "clang++" ]; then
export CFLAGS="-Qunused-arguments"
export CXXFLAGS="-Qunused-arguments"
sudo ln -s $(which ccache) /usr/lib/ccache/clang
sudo ln -s $(which ccache) /usr/lib/ccache/clang++
fi
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:
- ccache -M 1G
- ccache -z
- ${CC} --version
- ${CXX} --version
- |
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 REGRESSION_LEVEL=0 CVC4_REGRESSION_ARGS='--no-early-exit' ||
error "DISTCHECK (WITH NEWTHEORY TESTS) FAILED";
}
makeCheck() {
make V=1 -j2 check REGRESSION_LEVEL=0 CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/UNIT/SYSTEM/REGRESSION 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";
}
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_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}"
- ccache -s
matrix:
fast_finish: true
include:
# Test with GCC
- compiler: gcc
env:
- TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c --with-lfsc'
- compiler: gcc
env:
- TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --with-lfsc --disable-debug-symbols'
#
# Test with Clang
- compiler: clang
env:
- TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --with-cln --enable-gpl --disable-debug-symbols --disable-proof'
- compiler: clang
env:
- TRAVIS_CVC4=yes TRAVIS_CVC4_DISTCHECK=yes TRAVIS_CVC4_CONFIG='--enable-proof'
# Rule for running Coverity Scan.
- os: linux
compiler: gcc
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
|
