From a092506c8e029641c0668eef15b1f6e15fa5a3a9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 18 Mar 2021 09:45:24 +0100
Subject: [PATCH] drop support for Coq 8.11
---
.gitlab-ci.yml | 5 -----
CHANGELOG.md | 2 ++
README.md | 4 +++-
coq-iris.opam | 2 +-
4 files changed, 6 insertions(+), 7 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index de16cf2cf..5f157ca42 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -50,11 +50,6 @@ build-coq.8.12.2:
OPAM_PINS: "coq version 8.12.2"
DENY_WARNINGS: "1"
-build-coq.8.11.2:
- <<: *template
- variables:
- OPAM_PINS: "coq version 8.11.2"
-
# Nightly job with a known-to-work Coq version
# (so failures must be caused by std++)
build-stdpp.dev-coq.8.13.1:
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9ea121fed..f07e719dc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,8 @@ lemma.
## Iris master
+Coq 8.11 is no longer supported in this version of Iris.
+
**Changes in `algebra`:**
* Generalize the authorative elements of the `view`, `auth` and `gset_bij`
diff --git a/README.md b/README.md
index 2f66f3561..7808c83db 100644
--- a/README.md
+++ b/README.md
@@ -30,11 +30,13 @@ Importing Iris has some side effects as the library sets some global options.
This version is known to compile with:
- - Coq 8.11.2 / 8.12.2 / 8.13.1
+ - Coq 8.12.2 / 8.13.1
- A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
If you need to work with Coq 8.9 or Coq 8.10, you can use the
[iris-3.3 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.3).
+For a version compatible with Coq 8.11, check out the
+[iris-3.4 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.4).
### Working *with* Iris
diff --git a/coq-iris.opam b/coq-iris.opam
index e515bee60..1ff77cda0 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -13,7 +13,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo
"""
depends: [
- "coq" { (>= "8.11" & < "8.14~") | (= "dev") }
+ "coq" { (>= "8.12" & < "8.14~") | (= "dev") }
"coq-stdpp" { (= "dev.2021-03-23.0.c1266011") | (= "dev") }
]
--
GitLab