From a092506c8e029641c0668eef15b1f6e15fa5a3a9 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 18 Mar 2021 09:45:24 +0100 Subject: [PATCH 1/2] 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 From 6415d82a4e23b4f0077a007ddde4e86f246dda53 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 18 Mar 2021 09:55:08 +0100 Subject: [PATCH 2/2] remove now stale .ref files --- tests/proofmode_ascii.8.11.ref | 221 ------------------------------- tests/proofmode_monpred.8.11.ref | 89 ------------- 2 files changed, 310 deletions(-) delete mode 100644 tests/proofmode_ascii.8.11.ref delete mode 100644 tests/proofmode_monpred.8.11.ref diff --git a/tests/proofmode_ascii.8.11.ref b/tests/proofmode_ascii.8.11.ref deleted file mode 100644 index 684c4232b..000000000 --- a/tests/proofmode_ascii.8.11.ref +++ /dev/null @@ -1,221 +0,0 @@ -1 goal - - Σ : gFunctors - invG0 : invG Σ - cinvG0 : cinvG Σ - na_invG0 : na_invG Σ - N : namespace - P : iProp Σ - ============================ - "H" : inv N ( P) - "H2" : ▷ P - --------------------------------------□ - |={⊤ ∖ ↑N}=> ▷ P ∗ (|={⊤}=> ▷ P) - -1 goal - - Σ : gFunctors - invG0 : invG Σ - cinvG0 : cinvG Σ - na_invG0 : na_invG Σ - N : namespace - P : iProp Σ - ============================ - "H" : inv N ( P) - "H2" : ▷ P - --------------------------------------□ - "Hclose" : ▷ 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 γ ( P) - "HP" : ▷ P - --------------------------------------□ - "Hown" : cinv_own γ p - --------------------------------------∗ - |={⊤ ∖ ↑N}=> ▷ 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 γ ( P) - "HP" : ▷ P - --------------------------------------□ - "Hown" : cinv_own γ p - "Hclose" : ▷ 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 ( P) - "HP" : ▷ P - --------------------------------------□ - "Hown1" : na_own t E1 - "Hown2" : na_own t (E2 ∖ ↑N) - --------------------------------------∗ - |={⊤}=> (▷ 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 ( P) - "HP" : ▷ P - --------------------------------------□ - "Hown1" : na_own t E1 - "Hown2" : na_own t (E2 ∖ ↑N) - "Hclose" : ▷ 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))) diff --git a/tests/proofmode_monpred.8.11.ref b/tests/proofmode_monpred.8.11.ref deleted file mode 100644 index 2687a54f7..000000000 --- a/tests/proofmode_monpred.8.11.ref +++ /dev/null @@ -1,89 +0,0 @@ -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 ( 𝓟) ⎤ - "H2" : ⎡ ▷ 𝓟 ⎤ - --------------------------------------□ - |={⊤ ∖ ↑N}=> ⎡ ▷ 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤) - -1 goal - - I : biIndex - Σ : gFunctors - invG0 : invG Σ - N : namespace - 𝓟 : iProp Σ - ============================ - "H" : ⎡ inv N ( 𝓟) ⎤ - "H2" : ⎡ ▷ 𝓟 ⎤ - --------------------------------------□ - "Hclose" : ⎡ ▷ 𝓟 ={⊤ ∖ ↑N,⊤}=∗ emp ⎤ - --------------------------------------∗ - |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ 𝓟 ⎤ - -- GitLab