diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-20 21:33:13 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-20 21:33:13 +0100 |
commit | 8f337f072a3731dbb778afdb4a5882fd744333a4 (patch) | |
tree | 7cbfd7ce68b0e501b19299040b263fdb65d9fe79 /.gitlab-ci.yml | |
parent | 090dc09e4dbda97eea4ed28e67d84adf26f807f7 (diff) | |
download | compcert-kvx-8f337f072a3731dbb778afdb4a5882fd744333a4.tar.gz compcert-kvx-8f337f072a3731dbb778afdb4a5882fd744333a4.zip |
+k1c target
Diffstat (limited to '.gitlab-ci.yml')
-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 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" |