Merge branch 'ralf/coq-8.11' into 'master'

drop support for Coq 8.11

See merge request iris/iris!657

.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:

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`

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
 

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") }
 ]
 

tests/proofmode_ascii.8.11.ref

-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  cinvG0 : cinvG Σ
-  na_invG0 : na_invG Σ
-  N : namespace
-  P : iProp Σ
-  ============================
-  "H" : inv N (<pers> P)
-  "H2" : ▷ <pers> P
-  --------------------------------------□
-  |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
-  
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  cinvG0 : cinvG Σ
-  na_invG0 : na_invG Σ
-  N : namespace
-  P : iProp Σ
-  ============================
-  "H" : inv N (<pers> P)
-  "H2" : ▷ <pers> P
-  --------------------------------------□
-  "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
-  --------------------------------------∗
-  |={⊤ ∖ ↑N,⊤}=> ▷ P
-  
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  cinvG0 : cinvG Σ
-  na_invG0 : na_invG Σ
-  γ : gname
-  p : Qp
-  N : namespace
-  P : iProp Σ
-  ============================
-  _ : cinv N γ (<pers> P)
-  "HP" : ▷ <pers> P
-  --------------------------------------□
-  "Hown" : cinv_own γ p
-  --------------------------------------∗
-  |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
-  
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  cinvG0 : cinvG Σ
-  na_invG0 : na_invG Σ
-  γ : gname
-  p : Qp
-  N : namespace
-  P : iProp Σ
-  ============================
-  _ : cinv N γ (<pers> P)
-  "HP" : ▷ <pers> P
-  --------------------------------------□
-  "Hown" : cinv_own γ p
-  "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
-  --------------------------------------∗
-  |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
-  
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  cinvG0 : cinvG Σ
-  na_invG0 : na_invG Σ
-  t : na_inv_pool_name
-  N : namespace
-  E1, E2 : coPset
-  P : iProp Σ
-  H : ↑N ⊆ E2
-  ============================
-  _ : na_inv t N (<pers> P)
-  "HP" : ▷ <pers> P
-  --------------------------------------□
-  "Hown1" : na_own t E1
-  "Hown2" : na_own t (E2 ∖ ↑N)
-  --------------------------------------∗
-  |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
-          ∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
-  
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  cinvG0 : cinvG Σ
-  na_invG0 : na_invG Σ
-  t : na_inv_pool_name
-  N : namespace
-  E1, E2 : coPset
-  P : iProp Σ
-  H : ↑N ⊆ E2
-  ============================
-  _ : na_inv t N (<pers> P)
-  "HP" : ▷ <pers> P
-  --------------------------------------□
-  "Hown1" : na_own t E1
-  "Hown2" : na_own t (E2 ∖ ↑N)
-  "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ na_own t E2
-  --------------------------------------∗
-  |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
-  
-"test_iInv_12"
-     : string
-The command has indeed failed with message:
-Tactic failure: iInv: selector 34 is not of the right type .
-The command has indeed failed with message:
-Tactic failure: iInv: invariant nroot not found.
-The command has indeed failed with message:
-Tactic failure: iInv: invariant "H2" not found.
-"test_iInv"
-     : string
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  I : biIndex
-  N : namespace
-  E : coPset
-  𝓟 : iProp Σ
-  H : ↑N ⊆ E
-  ============================
-  "HP" : ⎡ ▷ 𝓟 ⎤
-  --------------------------------------∗
-  |={E ∖ ↑N}=> ⎡ ▷ 𝓟 ⎤ ∗ (|={E}=> emp)
-  
-"test_iInv_with_close"
-     : string
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  I : biIndex
-  N : namespace
-  E : coPset
-  𝓟 : iProp Σ
-  H : ↑N ⊆ E
-  ============================
-  "HP" : ⎡ ▷ 𝓟 ⎤
-  "Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
-  --------------------------------------∗
-  |={E ∖ ↑N,E}=> emp
-  
-"p1"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  forall (P : PROP) (_ : True), bi_entails P P
-"p2"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  forall P : PROP, and True (bi_entails P P)
-"p3"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  ex (fun P : PROP => bi_entails P P)
-"p4"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  bi_emp_valid (bi_exist (fun x : nat => bi_pure (eq x O)))
-"p5"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  bi_emp_valid (bi_exist (fun _ : nat => bi_pure (forall y : nat, eq y y)))
-"p6"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  ex
-    (unique
-       (fun z : nat =>
-        bi_emp_valid
-          (bi_exist
-             (fun _ : nat =>
-              bi_sep (bi_pure (forall y : nat, eq y y)) (bi_pure (eq z O))))))
-"p7"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  forall (a : nat) (_ : eq a O) (y : nat),
-  bi_entails (bi_pure True) (bi_pure (ge y O))
-"p8"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  forall (a : nat) (_ : eq a O) (y : nat), bi_emp_valid (bi_pure (ge y O))
-"p9"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  forall (a : nat) (_ : eq a O) (_ : nat),
-  bi_emp_valid (bi_forall (fun z : nat => bi_pure (ge z O)))

tests/proofmode_monpred.8.11.ref

-1 goal
-  
-  I : biIndex
-  PROP : bi
-  P, Q : monPred
-  i : I
-  ============================
-  "HW" : (P -∗ Q) i
-  --------------------------------------∗
-  (P -∗ Q) i
-  
-1 goal
-  
-  I : biIndex
-  PROP : bi
-  P, Q : monPred
-  i, j : I
-  ============================
-  "HW" : (P -∗ Q) j
-  "HP" : P j
-  --------------------------------------∗
-  Q j
-  
-1 goal
-  
-  I : biIndex
-  PROP : bi
-  P, Q : monPred
-  Objective0 : Objective Q
-  𝓟, 𝓠 : PROP
-  ============================
-  "H2" : ∀ i : I, Q i
-  "H3" : 𝓟
-  "H4" : 𝓠
-  --------------------------------------∗
-  ∀ i : I, 𝓟 ∗ 𝓠 ∗ Q i
-  
-1 goal
-  
-  I : biIndex
-  PROP : bi
-  FU : BiFUpd PROP
-  P, Q : monPred
-  i : I
-  ============================
-  --------------------------------------∗
-  (Q -∗ emp) i
-  
-1 goal
-  
-  I : biIndex
-  PROP : bi
-  FU : BiFUpd PROP
-  P : monPred
-  i : I
-  ============================
-  --------------------------------------∗
-  ∀ _ : (), ∃ _ : (), emp
-  
-The command has indeed failed with message:
-Tactic failure: iFrame: cannot frame (P i).
-1 goal
-  
-  I : biIndex
-  Σ : gFunctors
-  invG0 : invG Σ
-  N : namespace
-  𝓟 : iProp Σ
-  ============================
-  "H" : ⎡ inv N (<pers> 𝓟) ⎤
-  "H2" : ⎡ ▷ <pers> 𝓟 ⎤
-  --------------------------------------□
-  |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
-  
-1 goal
-  
-  I : biIndex
-  Σ : gFunctors
-  invG0 : invG Σ
-  N : namespace
-  𝓟 : iProp Σ
-  ============================
-  "H" : ⎡ inv N (<pers> 𝓟) ⎤
-  "H2" : ⎡ ▷ <pers> 𝓟 ⎤
-  --------------------------------------□
-  "Hclose" : ⎡ ▷ <pers> 𝓟 ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
-  --------------------------------------∗
-  |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ 𝓟 ⎤
-