aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitlab-ci.yml5
-rwxr-xr-xdev/ci/ci-basic-overlay.sh2
-rwxr-xr-xdev/ci/ci-menhir.sh8
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile4
4 files changed, 15 insertions, 4 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 99ae4c23ce..7dd9a37f59 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,7 +19,7 @@ stages:
variables:
# Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
# for reference]
- CACHEKEY: "bionic_coq-V2020-10-12-V89"
+ CACHEKEY: "bionic_coq-V2020-11-24-V90"
IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
# By default, jobs run in the base switch; override to select another switch
OPAM_SWITCH: "base"
@@ -784,6 +784,9 @@ library:ci-fiat_crypto_ocaml:
library:ci-flocq:
extends: .ci-template-flambda
+library:ci-menhir:
+ extends: .ci-template-flambda
+
library:ci-corn:
extends: .ci-template-flambda
stage: stage-4
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 75d9efaadc..18fdd83218 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -306,7 +306,7 @@
# menhirlib
########################################################################
# Note: menhirlib is now in subfolder coq-menhirlib of menhir
-: "${menhirlib_CI_REF:=master}"
+: "${menhirlib_CI_REF:=20201122}"
: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/menhir}"
: "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}"
diff --git a/dev/ci/ci-menhir.sh b/dev/ci/ci-menhir.sh
new file mode 100755
index 0000000000..5ad78383d8
--- /dev/null
+++ b/dev/ci/ci-menhir.sh
@@ -0,0 +1,8 @@
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download menhirlib
+
+( cd "${CI_BUILD_DIR}/menhirlib" && dune build @install -p menhirLib,menhirSdk,menhir && dune install -p menhirLib,menhirSdk,menhir menhir menhirSdk menhirLib --prefix=${CI_INSTALL_DIR} )
+
+( cd "${CI_BUILD_DIR}/menhirlib" && make -C coq-menhirlib && make -C coq-menhirlib install )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index c17ec502e7..195ac3152e 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-10-12-V89"
+# CACHEKEY: "bionic_coq-V2020-11-24-V90"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -42,7 +42,7 @@ ENV COMPILER="4.05.0"
# Common OPAM packages
ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
- CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
+ CI_OPAM="ocamlgraph.1.8.8" \
BASE_ONLY_OPAM="elpi.1.11.4"
# BASE switch; CI_OPAM contains Coq's CI dependencies.