diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 0e5c30934986c74666c16205c1f3a32457ef1936..a35e0442c25434ba4f0ced360645a8b6771f163c 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -32,6 +32,11 @@ build-coq.dev: variables: OPAM_PINS: "coq version dev" +build-coq.8.13.dev: + <<: *template + variables: + OPAM_PINS: "coq version 8.13.dev" + build-coq.8.12.1: <<: *template variables: @@ -48,11 +53,6 @@ build-coq.8.11.2: variables: OPAM_PINS: "coq version 8.11.2" -build-coq.8.10.2: - <<: *template - variables: - OPAM_PINS: "coq version 8.10.2" - # Nightly job with a known-to-work Coq version # (so failures must be caused by std++) build-stdpp.dev-coq.8.12.1: @@ -65,7 +65,7 @@ build-stdpp.dev-coq.8.12.1: - schedules - api -# Nightly job with latest Coq branch +# Nightly job with latest Coq beta branch build-stdpp.dev-coq.8.13.dev: <<: *template variables: diff --git a/CHANGELOG.md b/CHANGELOG.md index b5c07acdb187253e26a3f0d7a32b08e10f49e11a..4fe9f93ba689a48603aa4550f871a257ba0f8bea 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,7 +5,7 @@ lemma. ## Iris master -With this release, we dropped support for Coq 8.9. +With this release, we dropped support for Coq 8.9 and Coq 8.10. We also split Iris into multiple opam packages: `coq-iris` no longer contains HeapLang, which is now in a separate package `coq-iris-heap-lang`. diff --git a/README.md b/README.md index 26683828dc4c4c7ffa3d378fa7c724d26e490732..95722db7245240718af6bbcc53ce36d086683e35 100644 --- a/README.md +++ b/README.md @@ -30,7 +30,7 @@ Importing Iris has some side effects as the library sets some global options. This version is known to compile with: - - Coq 8.10.2 / 8.11.2 / 8.12.1 + - Coq 8.11.2 / 8.12.1 - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp) If you need to work with Coq 8.7 or Coq 8.8, please check out the diff --git a/coq-iris.opam b/coq-iris.opam index bed4bfb727fce02ad277b9168d6bf049bd734219..c93763e655ea7d3854412303bb82427012400b3e 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.10.2" & < "8.14~") | (= "dev") } + "coq" { (>= "8.11" & < "8.14~") | (= "dev") } "coq-stdpp" { (= "dev.2020-11-11.2.6385b547") | (= "dev") } ]