aboutsummaryrefslogtreecommitdiffstats
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-20 21:33:13 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-20 21:33:13 +0100
commit8f337f072a3731dbb778afdb4a5882fd744333a4 (patch)
tree7cbfd7ce68b0e501b19299040b263fdb65d9fe79 /.gitlab-ci.yml
parent090dc09e4dbda97eea4ed28e67d84adf26f807f7 (diff)
downloadcompcert-kvx-8f337f072a3731dbb778afdb4a5882fd744333a4.tar.gz
compcert-kvx-8f337f072a3731dbb778afdb4a5882fd744333a4.zip
+k1c target
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml11
1 files changed, 11 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index a285d8f2..9eafe558 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -87,3 +87,14 @@ build_rv32:
script:
- ./config_rv32.sh
- make -j "$NJOBS"
+
+build_k1c:
+ stage: build
+ image: "coqorg/coq"
+ before_script:
+ - opam switch 4.07.1+flambda
+ - eval `opam config env`
+ - opam install -y menhir
+ script:
+ - ./config_k1c.sh -no-runtime-lib
+ - make -j "$NJOBS"