blob: cff4612957a69cca84e64c38b977d4bc95af12d2 (
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
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
|
# This file used to contain configuration to also build documentation and CoqIDE,
# run the test-suite and the validate targets,
# including with 32-bits architecture or bleeding-edge compiler.
defaults:
params: ¶ms
# Following parameters are used in Coq CircleCI Job (using yaml
# reference syntax)
working_directory: ~/coq
docker:
- image: $CI_REGISTRY_IMAGE:$CACHEKEY
environment: &envvars
CACHEKEY: "bionic_coq-V2018-06-04-V2"
CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq
version: 2
before_script: &before_script
name: Setup OPAM Switch
command: |
echo export TERM=xterm >> ~/.profile
source ~/.profile
echo . ~/.profile >> $BASH_ENV
printenv | sort
opam switch "$COMPILER"
opam config list
opam list
.build-template: &build-template
<<: *params
steps:
- checkout
- run: *before_script
- run: &build-clean
name: Clean
command: |
make clean # ensure that `make clean` works on a fresh clone
- run: &build-configure
name: Configure
command: |
./configure -local -native-compiler ${NATIVE_COMP} -coqide no
- run: &build-build
name: Build
command: |
make -j ${NJOBS} byte
make -j ${NJOBS}
make test-suite/misc/universes/all_stdlib.v
- persist_to_workspace:
root: &workspace ~/
paths:
- coq/
environment:
<<: *envvars
NATIVE_COMP: "yes"
.ci-template: &ci-template
<<: *params
steps:
- run: *before_script
- attach_workspace: &attach_workspace
at: *workspace
- run:
name: Test
command: |
dev/ci/ci-wrapper.sh ${CIRCLE_JOB}
- persist_to_workspace:
root: *workspace
paths:
- coq/
environment: *envvars
# Defines individual jobs, see the workflows section below for job orchestration
jobs:
# Build and prepare test environment
build: *build-template
bignums:
<<: *ci-template
color:
<<: *ci-template
compcert:
<<: *ci-template
coq-dpdgraph:
<<: *ci-template
coquelicot:
<<: *ci-template
cross-crypto:
<<: *ci-template
elpi:
<<: *ci-template
equations:
<<: *ci-template
geocoq:
<<: *ci-template
fcsl-pcm:
<<: *ci-template
fiat-crypto:
<<: *ci-template
fiat-parsers:
<<: *ci-template
flocq:
<<: *ci-template
math-classes:
<<: *ci-template
corn:
<<: *ci-template
formal-topology:
<<: *ci-template
hott:
<<: *ci-template
iris-lambda-rust:
<<: *ci-template
ltac2:
<<: *ci-template
math-comp:
<<: *ci-template
mtac2:
<<: *ci-template
pidetop:
<<: *ci-template
sf:
<<: *ci-template
unimath:
<<: *ci-template
vst:
<<: *ci-template
workflows:
version: 2
# Run on each push
main:
jobs:
- build
- bignums: &req-main
requires:
- build
- color:
requires:
- build
- bignums
# - compcert: *req-main
# - coq-dpdgraph: *req-main
# - coquelicot: *req-main
# - cross-crypto: *req-main
# - elpi: *req-main
# - equations: *req-main
# - geocoq: *req-main
# - fcsl-pcm: *req-main
# - fiat-crypto: *req-main
# - fiat-parsers: *req-main
# - flocq: *req-main
- math-classes:
requires:
- build
- bignums
# - mtac2: *req-main
- corn:
requires:
- build
- math-classes
- formal-topology:
requires:
- build
- corn
# - hott: *req-main
# - iris-lambda-rust: *req-main
# - ltac2: *req-main
# - math-comp: *req-main
# - pidetop: *req-main
# - sf: *req-main
# - unimath: *req-main
# - vst: *req-main
|
