support Iris 4.3.0, Coq 8.20.0

.github/workflows/ci.yml

@@ -20,9 +20,9 @@ jobs:
         opam init
         opam repo add coq-released https://coq.inria.fr/opam/released
         opam update
-        opam pin coq 8.19.1 --confirm-level=yes
-        opam pin coq-iris 4.2.0 --confirm-level=yes
-        opam pin coq-iris-heap-lang 4.2.0 --confirm-level=yes
+        opam pin coq 8.20.0 --confirm-level=yes
+        opam pin coq-iris 4.3.0 --confirm-level=yes
+        opam pin coq-iris-heap-lang 4.3.0 --confirm-level=yes
 
     - name: Run check
       run: |

README.md

@@ -74,14 +74,14 @@ Using this technology, we have shown that storage protocols are useful for:
 
 # Getting started
 
-Leaf works with Iris 4.2.0 and is tested with Coq 8.19.1.
+Leaf works with Iris 4.3.0 and is tested with Coq 8.20.0.
 See [the Iris docs](https://gitlab.mpi-sws.org/iris/iris/) for more information about installing Iris.
 
 Make sure you have the right versions:
 
 ```
-opam pin coq 8.19.1
-opam pin coq-iris 4.2.0
+opam pin coq 8.20.0
+opam pin coq-iris 4.3.0
 ```
 
 ## Documentation and further reading

_CoqProject

@@ -52,3 +52,4 @@ src/examples/heap_lang_wp_load_shared.v
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -unknown-warning
 -arg -w -arg -argument-scope-delimiter
+-arg -w -arg -notation-incompatible-prefix

src/examples/counting.v

@@ -16,9 +16,6 @@ Require Import guarding.storage_protocol.protocol.
 
 Require Import examples.misc_tactics.
 
-Context {Σ: gFunctors}.
-Context `{!invGS Σ}.
-
 Definition COUNT_NAMESPACE := nroot .@ "count".
 
 Inductive Co :=

src/guarding/tactics.v

@@ -84,16 +84,16 @@ Qed.
 End TacticsHelpers.
 
 Tactic Notation "leaf_hyp" constr(g1) "rhs" "to" open_constr(Q) "as" constr(g2) :=
-  iPoseProof (guard_weaken_helper_right _ _ Q with (append g1 " []")) as g2.
+  iPoseProof (guard_weaken_helper_right _ _ Q with (String.append g1 " []")) as g2.
 
 Tactic Notation "leaf_hyp" constr(g1) "rhs" "to" open_constr(Q) "laters" "plus" open_constr(n) "as" constr(g2) :=
-  iPoseProof (guard_weaken_helper_right_laters_plus _ _ Q _ _ n with (append g1 " []")) as g2.
+  iPoseProof (guard_weaken_helper_right_laters_plus _ _ Q _ _ n with (String.append g1 " []")) as g2.
 
 Tactic Notation "leaf_hyp" constr(g1) "lhs" "to" open_constr(Q) "as" constr(g2) :=
-  iPoseProof (guard_weaken_helper_left Q with (append g1 " []")) as g2.
+  iPoseProof (guard_weaken_helper_left Q with (String.append g1 " []")) as g2.
 
 Tactic Notation "leaf_hyp" constr(g1) "lhs" "to" open_constr(Q) "laters" "plus" open_constr(n) "as" constr(g2) :=
-  iPoseProof (guard_weaken_helper_left_laters_plus Q _ _ _ _ n with (append g1 " []")) as g2.
+  iPoseProof (guard_weaken_helper_left_laters_plus Q _ _ _ _ n with (String.append g1 " []")) as g2.
 
 Tactic Notation "leaf_hyp" constr(g1) "mask" "to" open_constr(E) "as" constr(g2) :=
   iPoseProof (lguards_mask_weaken _ _ _ E with g1) as g2.
@@ -126,16 +126,15 @@ Tactic Notation "leaf_by_sep_except0" :=
   iApply lguards_weaken_except0; iModIntro.
 
 Tactic Notation "leaf_open" constr(g) "with" constr(sel) "as" constr(pat) :=
-  iMod (guards_open_helper with (append g (append " " sel))) as pat.
+  iMod (guards_open_helper with (String.append g (String.append " " sel))) as pat.
 
 Tactic Notation "leaf_open_laters" constr(g) "with" constr(sel) "as" constr(pat) :=
-  iMod (lguards_open_helper with (append g (append " " sel))) as pat.
+  iMod (lguards_open_helper with (String.append g (String.append " " sel))) as pat.
 
+Section TacticsTests.
 
 Context {Σ: gFunctors}.
 Context `{!invGS Σ}. 
-
-Section TacticsTests.
 
 Local Lemma test_leaf_hyp (A B C D : iProp Σ) E
     : (A &&{∅ ; 3}&&> B ∗ C) ⊢ (A ∗ D &&{E ; 20}&&> B).