Skip to content
Snippets Groups Projects
Commit 60cb1d82 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

split out 'make validate' into individual job

There's no need to run this for every compiler version; we only care
about the "main" version.
parent 25634fbd
No related branches found
No related tags found
No related merge requests found
# Taken from https://gitlab.com/erikmd/docker-coq-gitlab-ci-demo-1/blob/master/.gitlab-ci.yml
.build: .build:
stage: build stage: build
image: mathcomp/mathcomp:${CI_JOB_NAME} image: mathcomp/mathcomp:${CI_JOB_NAME}
script: script:
- ./create_makefile.sh - ./create_makefile.sh
- make -j ${NJOBS} - make -j ${NJOBS}
- make validate
1.8.0-coq-8.8: 1.8.0-coq-8.8:
extends: .build extends: .build
1.9.0-coq-8.9:
extends: .build
1.9.0-coq-dev: 1.9.0-coq-dev:
extends: .build extends: .build
# it's ok to fail with an unreleased version of Coq # it's ok to fail with an unreleased version of Coq
allow_failure: true allow_failure: true
1.9.0-coq-8.9:
extends: .build
# Keep track of all compiled output and the build infrastructure
artifacts:
name: build-files
paths:
- _CoqProject
- Makefile
- Makefile.conf
# Ugly hack around https://gitlab.com/gitlab-org/gitlab-runner/issues/2620
- "*/*.vo"
- "*/*/*.vo"
- "*/*/*/*.vo"
- "*/*/*/*/*.vo"
- "*/*/*/*/*/*.vo"
- "*/*/*/*/*/*/*.vo"
- "*/*/*/*/*/*/*/*.vo"
- "*/*/*/*/*/*/*/*/*.vo"
- "*/*/*/*/*/*/*/*/*/*.vo"
- "*/*.glob"
- "*/*/*.glob"
- "*/*/*/*.glob"
- "*/*/*/*/*.glob"
- "*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*/*/*/*.glob"
expire_in: 1 week
validate:
stage: test
image: mathcomp/mathcomp:1.9.0-coq-8.9
dependencies:
- 1.9.0-coq-8.9
script: make validate
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment