diff options
| author | Erik Martin-Dorel | 2018-12-20 16:24:14 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2018-12-21 12:17:14 +0100 |
| commit | ab8aefdcff6cf02e8cfe51bd052242f9907c5e72 (patch) | |
| tree | 80adde7d489d86b9d69f1d9ae29ee527006ad996 /.gitlab-ci.yml | |
| parent | da5985eae6656be1bd30aee76c8d08dbc3a09c25 (diff) | |
Add hidden job .make-build to also test the Makefile build infra
* This job is only instantiated with coqorg/coq:latest
* Add the associated Dockerfile.make
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 6c70f50..b8c9c8f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -70,6 +70,28 @@ coq-8.8: coq-dev: extends: .opam-build +# 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: + 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 CONTRIB_URL, script, COQ_VERSION, CONTRIB_VERSION when using .ci: stage: test |