diff options
| author | Enrico Tassi | 2019-01-09 14:01:51 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-10 16:39:50 +0100 |
| commit | 325f7ffb27496c8017d50712fe100658ea39bf2b (patch) | |
| tree | 5b48fb07bb193772d672aeccf4c55016c9e07356 | |
| parent | 468050a3831cedf63d7dbdb289d5824097bbe1e0 (diff) | |
[ci] compile with -quick & validate after vio2vo
| -rw-r--r-- | .gitlab-ci.yml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f54f64bf28..413836f956 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -245,6 +245,12 @@ build:base+async: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" COQUSERFLAGS: "-async-proofs on" +build:quick: + <<: *build-template + variables: + COQ_EXTRA_CONF: "-native-compiler no" + QUICK: "1" + windows64: <<: *windows-template variables: @@ -454,6 +460,11 @@ validate:edge+flambda: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" +validate:quick: + <<: *validate-template + dependencies: + - build:quick + # Libraries are by convention the projects that depend on Coq # but not on its ML API |