blob: 270bdcaedec7987d224c2ee3caf3d978a820db2c (
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
|
dist: trusty
# Travis builds are slower using sudo: false (the container-based
# infrastructure) as of March 2017; see
# https://github.com/coq/coq/pull/467 for some discussion.
sudo: required
# Until Ocaml becomes a language, we set a known one.
language: c
cache:
apt: true
directories:
- $HOME/.opam
addons:
apt:
sources:
- avsm
packages:
- opam
- aspcud
- gcc-multilib
env:
global:
- NJOBS=2
# system is == 4.02.3
- COMPILER="system"
# Main test suites
matrix:
- TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
- TEST_TARGET="validate" TW="travis_wait"
- TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait"
- TEST_TARGET="ci-bedrock-src"
- TEST_TARGET="ci-bedrock-facade"
- TEST_TARGET="ci-color"
- TEST_TARGET="ci-compcert"
- TEST_TARGET="ci-coquelicot"
- TEST_TARGET="ci-geocoq"
- TEST_TARGET="ci-fiat-crypto"
- TEST_TARGET="ci-fiat-parsers"
- TEST_TARGET="ci-flocq"
- TEST_TARGET="ci-formal-topology"
- TEST_TARGET="ci-hott"
- TEST_TARGET="ci-iris-coq"
- TEST_TARGET="ci-math-classes"
- TEST_TARGET="ci-math-comp"
- TEST_TARGET="ci-sf"
- TEST_TARGET="ci-unimath"
- TEST_TARGET="ci-vst"
# Not ready yet for 8.7
# - TEST_TARGET="ci-cpdt"
# - TEST_TARGET="ci-metacoq"
# - TEST_TARGET="ci-tlc"
matrix:
allow_failures:
- env: TEST_TARGET="ci-geocoq"
- env: TEST_TARGET="ci-vst"
# Full Coq test-suite with two compilers
# [TODO: use yaml refs and avoid duplication for packages list]
include:
- env:
- TEST_TARGET="test-suite"
- EXTRA_CONF="-coqide opt -with-doc yes"
- EXTRA_OPAM="lablgtk-extras hevea"
addons:
apt:
sources:
- avsm
packages:
- opam
- aspcud
- libgtk2.0-dev
- libgtksourceview2.0-dev
- texlive-latex-base
- texlive-latex-recommended
- texlive-latex-extra
- texlive-math-extra
- texlive-fonts-recommended
- texlive-fonts-extra
- latex-xcolor
- ghostscript
- transfig
- imagemagick
- env:
- TEST_TARGET="test-suite"
- COMPILER="4.04.0"
- EXTRA_CONF="-coqide opt -with-doc yes"
- EXTRA_OPAM="lablgtk-extras hevea"
addons:
apt:
sources:
- avsm
packages:
- opam
- aspcud
- libgtk2.0-dev
- libgtksourceview2.0-dev
- texlive-latex-base
- texlive-latex-recommended
- texlive-latex-extra
- texlive-math-extra
- texlive-fonts-recommended
- texlive-fonts-extra
- latex-xcolor
- ghostscript
- transfig
- imagemagick
install:
- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
- eval $(opam config env)
- opam config var root
- opam install -j ${NJOBS} -y camlp5 ocamlfind ${EXTRA_OPAM}
- opam list
script:
- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
- ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF}
- echo -en 'travis_fold:end:coq.config\\r'
- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
- make -j ${NJOBS}
- echo -en 'travis_fold:end:coq.build\\r'
- echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r'
- ${TW} make -j ${NJOBS} ${TEST_TARGET}
- echo -en 'travis_fold:end:coq.test\\r'
|
