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
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
|
# Design:
# - build stage (e.g. docker build -t mathcomp-dev:$IID_$SLUG_coq-8.7 .)
# - choice of the OCaml compiler: var OPAM_SWITCH in {base, edge}
# (Dockerfile containing: "opam switch set $compiler && eval $(opam env)")
# - all branches (not tags) => push on GitLab registry
# - GitHub PRs => push on GitLab and report back thanks to @coqbot
# - test stage (image: mathcomp-dev:$IID_$SLUG_coq-8.6)
# - script template foreach project (custom CONTRIB_URL, script)
# - jobs foreach project and Coq version (custom COQ_VERSION, CONTRIB_VERSION)
# - deploy stage (only branch "master" and environment "deployment")
# - pull each built image from GitLab registry => push to Docker Hub
#
# Config for protected environment "deployment":
# - set vars HUB_REGISTRY, HUB_REGISTRY_USER, HUB_REGISTRY_IMAGE, HUB_TOKEN
#
# Remark:
# - The name chosen for branches should ideally yield different values
# of CI_COMMIT_REF_SLUG.
# - But this is not mandatory as image tags start with "${CI_PIPELINE_IID}_".
# cf. doc:
# - CI_COMMIT_REF_NAME: The branch or tag name for which project is built.
# - CI_COMMIT_REF_SLUG: $CI_COMMIT_REF_NAME lowercased, shortened to 63 bytes,
# and with everything except 0-9 and a-z replaced with -.
# No leading / trailing -. Use in URLs, host names and domain names.
# - CI_PIPELINE_IID: The unique id of the current pipeline scoped to project.
stages:
- build
- deploy
- test
################
#### build stage
################
# set var OPAM_SWITCH (if need be) and COQ_VERSION when using
.make-build:
stage: build
image: docker:latest
services:
- docker:dind
variables:
# This image will be built locally only (not pushed)
IMAGE: "mathcomp-dev:make_coq-${COQ_VERSION}"
OPAM_SWITCH: "edge"
before_script:
- echo "${OPAM_SWITCH}"
- echo "${COQ_VERSION}"
script:
- docker build -f Dockerfile.make --pull --build-arg=coq_image="coqorg/coq:${COQ_VERSION}" --build-arg=compiler="${OPAM_SWITCH}" -t "${IMAGE}" .
except:
- tags
- merge_requests
make-coq-latest:
extends: .make-build
variables:
COQ_VERSION: "latest"
# set var OPAM_SWITCH (if need be) when using
.opam-build:
stage: build
image: docker:latest
services:
- docker:dind
variables:
IMAGE: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}_${CI_JOB_NAME}"
OPAM_SWITCH: "edge"
before_script:
- echo "${OPAM_SWITCH}"
- echo "${CI_JOB_TOKEN}" | docker login -u "${CI_REGISTRY_USER}" --password-stdin "${CI_REGISTRY}"
script:
- docker build --pull --build-arg=coq_image="coqorg/${CI_JOB_NAME//-/:}" --build-arg=compiler="${OPAM_SWITCH}" -t "${IMAGE}" .
- docker push "${IMAGE}"
- docker logout "${CI_REGISTRY}"
except:
- tags
- merge_requests
coq-8.7:
extends: .opam-build
coq-8.8:
extends: .opam-build
coq-8.9:
extends: .opam-build
coq-dev:
extends: .opam-build
################
##### test stage
################
# set CONTRIB_URL, script, COQ_VERSION, CONTRIB_VERSION when using
.ci:
stage: test
image: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}_coq-${COQ_VERSION}"
variables:
GIT_STRATEGY: none
before_script:
- cat /proc/{cpu,mem}info || true
# don't printenv to avoid cluttering the log
- opam config list
- opam repo list
- opam list
- coqc --version
- echo "${COQ_VERSION}"
- echo "${CONTRIB_URL}"
- echo "${CONTRIB_VERSION}"
- git clone -b "${CONTRIB_VERSION}" --depth 1 "${CONTRIB_URL}" /home/coq/ci
- cd /home/coq/ci
- git rev-parse --verify HEAD
- git describe --all --long --abbrev=40 --always --dirty
except:
- tags
- merge_requests
# Guidelines to add a library to mathcomp CI:
# - Add a hidden job (starting with a .) .ci-lib that extends the .ci job,
# sets var CONTRIB_URL (library Git URL), and defines a dedicated script
# - Add 1 job per Coq version to test, that extends the previous hidden job,
# and sets vars COQ_VERSION, CONTRIB_VERSION (compatible Git branch/tag)
# The Four Color Theorem
.ci-fourcolor:
extends: .ci
variables:
CONTRIB_URL: "https://github.com/math-comp/fourcolor.git"
CONTRIB_VERSION: master
script:
- make -j "${NJOBS}"
- make install
ci-fourcolor-8.7:
extends: .ci-fourcolor
variables:
COQ_VERSION: "8.7"
ci-fourcolor-8.8:
extends: .ci-fourcolor
variables:
COQ_VERSION: "8.8"
ci-fourcolor-dev:
extends: .ci-fourcolor
variables:
COQ_VERSION: "dev"
# The Odd Order Theorem
.ci-odd-order:
extends: .ci
variables:
CONTRIB_URL: "https://github.com/math-comp/odd-order.git"
CONTRIB_VERSION: master
script:
- make -j "${NJOBS}"
- make install
ci-odd-order-8.7:
extends: .ci-odd-order
variables:
COQ_VERSION: "8.7"
# The Lemma Overloading library
.ci-lemma-overloading:
extends: .ci
variables:
CONTRIB_URL: "https://github.com/coq-community/lemma-overloading.git"
CONTRIB_VERSION: master
script:
- opam pin add -n -k path coq-lemma-overloading .
- opam install -y -v -j "${NJOBS}" coq-lemma-overloading
ci-lemma-overloading-8.8:
extends: .ci-lemma-overloading
variables:
COQ_VERSION: "8.8"
ci-lemma-overloading-8.9:
extends: .ci-lemma-overloading
variables:
COQ_VERSION: "8.9"
ci-lemma-overloading-dev:
extends: .ci-lemma-overloading
variables:
COQ_VERSION: "dev"
################
### deploy stage
################
# Changes below (or jobs extending .docker-deploy) should be carefully
# reviewed to avoid leaks of HUB_TOKEN
.docker-deploy:
stage: deploy
image: docker:latest
services:
- docker:dind
environment:
name: deployment
url: https://hub.docker.com/r/mathcomp/mathcomp-dev
variables:
HUB_IMAGE: "mathcomp/${CI_JOB_NAME}"
IMAGE_PREFIX: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}"
script:
- export IMAGE="${IMAGE_PREFIX}_${CI_JOB_NAME##*:}"
- echo "${IMAGE}"
- docker pull "${IMAGE}"
- echo "${HUB_IMAGE}"
- docker tag "${IMAGE}" "${HUB_IMAGE}"
- test -n "${HUB_REGISTRY}"
- test -n "${HUB_REGISTRY_USER}"
- echo "${HUB_TOKEN}" | docker login -u "${HUB_REGISTRY_USER}" --password-stdin "${HUB_REGISTRY}"
- docker push "${HUB_IMAGE}"
- docker logout "${HUB_REGISTRY}"
only:
- master
mathcomp-dev:coq-8.7:
extends: .docker-deploy
mathcomp-dev:coq-8.8:
extends: .docker-deploy
mathcomp-dev:coq-8.9:
extends: .docker-deploy
mathcomp-dev:coq-dev:
extends: .docker-deploy
|
