From afeb6f079ad1c440dfc34b1100824db27c60fe19 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 May 2023 20:57:54 +0200
Subject: [PATCH] Bump Iris. Bump Coq version to 8.17.
---
.gitlab-ci.yml | 10 +++++-----
README.md | 2 +-
_CoqProject | 2 ++
coq-iris-examples.opam | 2 +-
4 files changed, 9 insertions(+), 7 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 08a8a4a3..31da8a15 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -47,11 +47,11 @@ build-coq.dev:
variables:
OPAM_PINS: "coq version dev"
-build-coq.8.15.0:
+build-coq.8.17.0:
<<: *template
variables:
OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
- OPAM_PINS: "coq version 8.15.0"
+ OPAM_PINS: "coq version 8.17.0"
DENY_WARNINGS: "1"
MANGLE_NAMES: "1"
# Coq bench needs an opam package
@@ -60,11 +60,11 @@ build-coq.8.15.0:
- fp-timing
# Separate MR job that does not run on fp-timing.
-build-coq.8.15.0-mr:
+build-coq.8.17.0-mr:
<<: *template
<<: *only_mr
variables:
- OPAM_PINS: "coq version 8.15.0"
+ OPAM_PINS: "coq version 8.17.0"
MANGLE_NAMES: "1"
DENY_WARNINGS: "1"
@@ -72,7 +72,7 @@ trigger-iris.timing:
<<: *template
variables:
OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
- OPAM_PINS: "coq version 8.15.0 git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+ OPAM_PINS: "coq version 8.17.0 git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
tags:
- fp-timing
only:
diff --git a/README.md b/README.md
index a9cbc3e6..fbcf8484 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ Some example verification demonstrating the use of Iris.
This version is known to compile with:
- - Coq 8.15.0
+ - Coq 8.17.0
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
- A development version of [Autosubst](https://github.com/coq-community/autosubst)
diff --git a/_CoqProject b/_CoqProject
index a5316e76..2d5f7bce 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,6 +4,8 @@
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
+# Fixing this one requires Coq 8.17
+-arg -w -arg -future-coercion-class-field
theories/barrier/proof.v
theories/barrier/specification.v
diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index 5f2b5988..a8a9b317 100644
--- a/coq-iris-examples.opam
+++ b/coq-iris-examples.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
depends: [
- "coq-iris-heap-lang" { (= "dev.2023-04-12.0.958aad09") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2023-05-02.4.943e9b74") | (= "dev") }
"coq-autosubst" { = "dev" }
]
--
GitLab