aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/docker/bionic_coq
diff options
context:
space:
mode:
authorVincent Laporte2018-11-06 13:21:13 +0000
committerVincent Laporte2018-11-06 13:28:40 +0000
commitd6a5b036ba11850441afe86dedfe8f3591df9cad (patch)
treee5e9ebdf1dfeda2442819251eb813fd0965765ca /dev/ci/docker/bionic_coq
parentf6033667bd9b8069308d4bcba420c4ce0771e44f (diff)
[Docker] Update COMPILER_EDGE: 4.07.0 → 4.07.1
Also update CAMLP5_VER_EDGE: 7.06 → 7.06.10-g84ce6cc4 This is to avoid an OCaml bug that occurs when compiling the OCaml code extracted from part of a patched version of CompCert. ~~~ File "extraction/Parser.ml", line 12375, characters 19-29: Error: Constraints are not satisfied in this type. Type initstate' should be an instance of initstate' ~~~ This compiler issue only appears with OCaml 4.07.0 (neither with 4.06 nor with 4.07.1); hence this update.
Diffstat (limited to 'dev/ci/docker/bionic_coq')
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile6
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 098c950b32..4ddb582414 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-10-23-V1"
+# CACHEKEY: "bionic_coq-V2018-10-30-V1"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -53,8 +53,8 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
opam install $BASE_OPAM camlp5.$CAMLP5_VER
# EDGE switch
-ENV COMPILER_EDGE="4.07.0" \
- CAMLP5_VER_EDGE="7.06" \
+ENV COMPILER_EDGE="4.07.1" \
+ CAMLP5_VER_EDGE="7.06.10-g84ce6cc4" \
COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
BASE_OPAM_EDGE="dune-release.1.1.0"