blob: 044e43d45089831e79be04e8951634542e08b5cb (
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
|
# 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:
- 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
[ -z "$TRAVIS_CVC4" ] && 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'
notifications:
email:
on_success: change
on_failure: always
|
