.gitignore

@@ -23,3 +23,5 @@ Makefile.coq.conf
 Makefile.package.*
 .Makefile.package.*
 _opam
+_build
+*.install

.gitlab-ci.yml

@@ -45,10 +45,10 @@ variables:
 ## Build jobs
 
 # The newest version runs with timing.
-build-coq.8.18.0:
+build-coq.8.20.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.18.0"
+    OPAM_PINS: "coq version 8.20.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
     OPAM_PKG: "1"
@@ -59,28 +59,28 @@ build-coq.8.18.0:
   interruptible: false
 
 # The newest version also runs in MRs, without timing.
-build-coq.8.18.0-mr:
+build-coq.8.20.0-mr:
   <<: *template
   <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.18.0"
+    OPAM_PINS: "coq version 8.20.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
-build-coq.8.17.1:
+# Also ensure Dune works.
+build-coq.8.20.0-dune:
   <<: *template
+  <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.17.1"
-    DENY_WARNINGS: "1"
-    MANGLE_NAMES: "1"
+    OPAM_PINS: "coq version 8.20.0   dune version 3.15.2"
+    MAKE_TARGET: "dune"
 
 # The oldest version runs in MRs, without name mangling.
-build-coq.8.16.1:
+build-coq.8.19.2:
   <<: *template
   <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.16.1"
-    DENY_WARNINGS: "1"
+    OPAM_PINS: "coq version 8.19.2"
 
 trigger-stdpp.dev:
   <<: *template

CHANGELOG.md

@@ -3,9 +3,258 @@ way the logic is used on paper.  We also document changes in the Coq
 development; every API-breaking change should be listed, but not every new
 lemma.
 
-## Iris master
+## Iris 4.3.0 (2024-10-30)
+
+This Iris release mostly features quality-of-life improvements, such as
+improvements to `iInduction`, a new `iUnfold` tactic, and improved errors
+in `iInv`. Furthermore, like std++, Iris can now be built with dune.
+
+Iris 4.3.0 supports Coq 8.19 and 8.20. Coq 8.18 is no longer supported.
+
+This release was managed by Jesper Bengtson, Ralf Jung and Robbert Krebbers, 
+with contributions from Benjamin Peters, Isaac van Bakel, Jan-Oliver Kaiser,
+Janggun Lee, Michael Sammler, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre
+Sanjit Bhat, Tej Chajed, William Mansky, and Yusuke Matsushita.
+Thanks a lot to everyone involved!
+
+
+**Changes in `algebra`:**
+
+* Add lemmas `big_opS_gset_to_gmap` and `big_opS_gset_to_gmap_L`, which rewrite
+  between `gset_to_gmap` and big set ops of singleton maps.  (by Isaac van
+  Bakel)
+* Add lemmas `discrete_fun_update` and `discrete_fun_updateP`, which updates an
+  abitrary `discrete_fun` to another. For `discrete_fun_updateP`, this requires
+  the domain to be finite, similar to `discrete_fun_included_spec`. (by Janggun Lee)
+* Add lemmas `discrete_fun_singleton_valid` and `discrete_fun_singleton_unit`, which simplify 
+  cmra validity and unit used with `discrete_fun_singleton`. (by Janggun Lee)
+* Add `Inhabited` instance for the solution of the COFE solver.
+
+**Changes in `bi`:**
+
+* Add instances for `match _ with _ end` (and thus `if _ then _ else` and
+  `'(_, _)` pair destructuring) for `Persistent`, `Affine`, `Absorbing`,
+  `Timeless`, and `Plain`. (by Sanjit Bhat)
+
+**Changes in `proofmode`:**
+
+* Remove the `*` specialization pattern. This pattern has been deprecated and a
+  no-op since 2017. See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/41.
+* Improve the error message of `iInv` in case the goal does not support
+  invariant opening.
+* Change `iInduction` to always generate a magic wand instead of sometimes
+  generating an implication for reverted hypotheses.
+* Add `iUnfold` tactic.
+* Improve ability to name induction hypotheses (IHs) in `iInduction`: when
+  performing `iInduction x as cpat` the names of the IHs in the Coq introduction
+  pattern `cpat` are used to name the IHs in the proof mode context. For
+  example, `iInduction n as [|n IH]` and `iInduction t as [|l IHl r IHr]`.
+
+**Changes in `base_logic`:**
+
+* Add lemma `na_own_empty` and persistence instance for `na_own p ∅` for
+  non-atomic invariant tokens. (by Benjamin Peters)
+* Add instances `big_sepL_flip_mono'`, `big_sepM_flip_mono'`, etc., which are
+  wrappers of instances `big_sep*_mono'` for `flip (⊢)` instead of `(⊢)`. (by
+  Yusuke Matsushita)
+
+**Changes in `program_logic`:**
+
+* Add missing proofmode instances for error reporting and opening invariants
+  around total weakest preconditions. (by Janggun Lee)
+
+**Changes in `heap_lang`:**
+
+* Make `wp_cmpxchg_fail` work when the points-to is in the persistent context.
+* Seal definition of `pointsto`, add copies of all relevant lemmas.
+
+**Infrastructure:**
+
+* Add support for compiling the packages with dune. (by Rodolphe Lepigre) 
+
+
+## Iris 4.2.0 (2024-04-12)
+
+The highlights of this release are:
+* We have new laws to "undiscard" discarded fractions, allowing one to update
+  from `DfracDiscarded` to `DfracOwn(q)` for some fresh `q`. This gives rise to
+  new laws for all constructions that use `dfrac`, such as
+  `ghost_map_elem_unpersist : ∀ k γ v, k ↪[γ]□ v ==∗ ∃ q, k ↪[γ]{#q} v`.
+* The `gmap_view K V` camera now supports value types `V` that are arbitrary
+  cameras, and lifts their composition to the whole map. The previous `gmap_view`
+  type can be recovered as `gmap_view K (agree V)`.
+* The `iFrame` tactic has become stronger for goals that contain existential
+  quantifiers: `iFrame` will now attempt to instantiate these. For example,
+  framing `P x` in goal `Q ∗ ∃ y, P y ∗ R` will now succeed with remaining
+  goal `Q ∗ R`.
+
+Iris 4.2 supports Coq 8.18 and 8.19.
+Coq 8.16 and 8.17 are no longer supported.
+
+This release was managed by Ralf Jung and Robbert Krebbers, with contributions
+from Ike Mulder, Jan-Oliver Kaiser, Johannes Hostert, Pierre Roux, Thomas
+Somers, and Yixuan Chen. Thanks a lot to everyone involved!
+
+**Changes in `algebra`:**
+
+* Rename `discrete` to `discrete_0`, to make room for a new lemma `discrete`
+  that works for all `n` : `x ≡{n}≡ y → x ≡ y`.
+* Enable `f_equiv` and `solve_proper` to exploit the fact that `≡{n}≡` is a
+  subrelation of `≡` and `=`.
+* Rename `iso_cmra_mixin_restrict` to `iso_cmra_mixin_restrict_validity`, and
+  simplify its statement and that of `iso_cmra_mixin` by removing the `g_equiv`
+  assumption that follows from the other assumptions.
+* Add `inj_cmra_mixin_restrict_validity` as a more general version of
+  `iso_cmra_mixin_restrict_validity`.
+* Change statement of `Z_local_update` to be more intuitive. It now says
+  `x - y = x' - y' → (x,y) ~l~> (x',y')`, i.e., the difference between the
+  authoritative element and the fragment must stay the same.
+* Rename `cmra_discrete_update` → `cmra_discrete_total_update` and
+  `cmra_discrete_updateP` → `cmra_discrete_total_updateP`. Repurpose original
+  names for lemmas that only require `CmraDiscrete`, not `CmraTotal`.
+* Add a law for undiscarding discarded fractions, allowing one to update from
+  `DfracDiscarded` to `DfracOwn(q)` for some fresh `q`. This formalizes the
+  intuition that a discarded fraction is merely an "existentially quantified
+  fraction." (by Johannes Hostert)
+* Add laws for un-persisting resources with a discardable fractional part,
+  based on the undiscarding law for discardable fractions. For example,
+  `gmap_view_frag k DfracDiscarded v ~~>: λ a, ∃ q, a = gmap_view_frag k (DfracOwn q) v`
+  will allow recovering a fractional points-to from a discarded one. (by Johannes
+  Hostert)
+* Generalize `gmap_viewUR K A` from `A : ofe` to `A : cmra`. Previously, the
+  "agreement" camera was part of the definition, now the user can pick an
+  arbitrary camera. All lemmas that exposed agreement properties have
+  been generalized to expose general camera validity/composition.
+  For porting:
+  + Replace `gmap_viewR K V` by `gmap_viewR K (agreeR V)`.
+  + Definitions and proofs on top of this will need to be manually adjusted.
+  + Replace `gmap_view_update` by `gmap_view_replace`.
+  + Proofs using `gmap_view_both_dfrac_valid_L` should instead use
+    `gmap_view_both_dfrac_valid_discrete_total` followed by `to_agree_included_L`.
+
+**Changes in `proofmode`:**
+
+* The `iFrame` tactic has become slightly weaker for goals that contain both
+  evars and either `∨` or `∧`. This prevents an exponential slowdown of
+  `iFrame` on some goals. This change should be backwards compatible for almost
+  all proofs. If you define or use custom `Frame` instances, note that the 
+  `MaybeFrame` class has become notation for `TCNoBackTrack (MaybeFrame' ...)`,
+  which means the proofs of your instances might need a slight refactoring.
+* Adjust the `iFrame` proof search to use `QuickAffine` and `QuickAbsorbing`
+  instead of `Affine` and `Absorbing`. This fixes some performance issues with
+  large terms in non-affine logics, at the expense of a slight reduction in what
+  `iFrame` can do in these logics.
+* The `iFrame` tactic has become stronger for goals that contain existential
+  quantifiers: `iFrame` will now attempt to instantiate these. For example,
+  framing `P x` in goal `Q ∗ ∃ y, P y ∗ R` will now succeed with remaining
+  goal `Q ∗ R`. `iFrame` still behaves the same when no instantiation can be
+  found: framing `R` in goal `Q ∗ ∃ y, P y ∗ R` still gives `Q ∗ ∃ y, P y`.
+  This should simplify and potentially even speed up some proofs (MR: iris/iris!1017).  
+  Porting to this change will require manually fixing broken proofs: `iFrame`
+  may now make more progress than your proof script expects. Proofs that look
+  like `iFrame. iExists _. iFrame.` may need to be replaced with just `iFrame.`
+  In some cases, you may need to be explicit in what hypotheses to `iFrame`,
+  to prevent wrong instantiation of existential quantifiers.  
+  To temporarily fix broken proofs, you can restore `iFrame`'s old behavior with:
+  ```
+  Local Instance frame_exist_instantiate_disabled :
+    FrameInstantiateExistDisabled := {}.
+  ```
+  `iFrame` will not instantiate existential quantifiers below connectives such as
+  `-∗`, `∀`, `→` and `WP`, since this is more frequently unsafe (MR: iris/iris!1035).
+  If you have custom recursive `Frame` instances for which you want to disable 
+  instantiating existential quantifiers, you need to replace the `Frame ...` premise
+  of your instance with `(FrameInstantiateExistDisabled → Frame ...)`.
+* `iFrame` no longer loops on `[∗mset ] x ∈ X, ..` when `X` is an existential variable 
+   (MR: iris/iris!1039). (by Jan-Oliver Kaiser for BedRock Systems)
+
+**Changes in `base_logic`:**
+
+* Rename `mapsto` to `pointsto` to align with standard separation logic
+  terminology.
+* Add laws for un-persisting assertions with a discardable fractional permission,
+  for example `l ↦□ v ==∗ ∃ q, l ↦{#q} v`, using the new laws from `algebra`
+  (see above). These laws allow one to update a persistent (discarded) assertion,
+  like a points-to, back into a fractionally owned one, where the fraction is
+  existentially quantified. They are useful when e.g. constructing invariants
+  that allow exchanging fractional assertions. See !960 for more details. (by
+  Johannes Hostert)
+* Add `token` library, providing a simple ghost token as a logic-level wrapper
+  over the RA `excl unit`.
+* Add lemma `lc_fupd_add_laterN`. (by Thomas Somers)
+
+**Changes in `program_logic`:**
+
+* Rename `head_step` to `base_step` to avoid potential confusion with the
+  standard term "head reduction", and also rename all associated definitions and
+  lemmas. In particular: `head_stuck` → `base_stuck`, `head_reducible` →
+  `base_reducible`, `head_irreducible` → `base_irreducible`, `head_redex` →
+  `base_redex`, `head_atomc` → `base_atomic`. The sed script will rename all
+  definitions and lemmas that come with Iris, but if you had additional
+  definitions or lemmas with `head` in their name, you will have to rename them
+  by hand if you want to remain consistent.
+
+**Changes in `heap_lang`:**
+
+* Replace `wp_lb_init` with a more general `steps_lb_0` lemma for creating a
+  `steps_lb` without depending on WP. (by Thomas Somers)
+* Add generic lemma `twp_wp_step_lc` to derive WP with later credits from TWP.
+* Add Texan triples with later credits for stateful operations: `wp_alloc_lc`,
+  `wp_alloc_lc`, `wp_free_lc`, `wp_load_lc`, `wp_store_lc`, `wp_xchg_lc`,
+  `wp_cmpxchg_fail_lc`, `wp_cmpxchg_suc_lc`, and `wp_faa_lc`.
+
+The following `sed` script helps adjust your code to the renaming (on macOS,
+replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# discrete camera updates
+s/\bcmra_discrete_update\b/cmra_discrete_total_update/g
+s/\bcmra_discrete_updateP\b/cmra_discrete_total_updateP/g
+# maps-to → points-to
+s/(\b|_)mapsto(\b|_)/\1pointsto\2/g
+# Head reduction
+s/(\b|_)head_(step|stuck|ctx|prim_|(ir)?reducible)/\1\base_\2/g
+EOF
+```
+
+## Iris 4.1.0 (2023-10-11)
+
+This Iris release mostly features quality-of-life improvements, such as smarter
+handling of `->`/`<-` patterns by `iDestruct`, support for an arbitrary number of
+Coq intro patterns in the Iris proofmode tactics (`iIntros`, `iDestruct`, etc.),
+and support for immediately introducing the postcondition of a WP specification
+via `wp_apply lemma as "Hpost"`.
+
+The biggest changes and new features are:
+* Logically atomic triples now support private (non-atomic) postconditions, and
+  the notation was changed to not clash with Autosubst any more. Existing users
+  of logically atomic specifications have to update their notation, see the full
+  CHANGELOG for more details.
+* The meaning of `P -∗ Q` as a Coq proposition has changed from `P ⊢ Q` to
+  `⊢ P -∗ Q`. If you are only using the Iris proofmode, this will not make a
+  difference, but when writing proof scripts or tactics that `rewrite` or
+  `apply` Iris lemmas, the exact position of the `⊢ P -∗ Q` matters and this
+  will now always be visible in lemma statements.
+* `iCombine` is starting to gain support for a `gives` clause, which yields
+  persistent facts gained from combining the resources. So far, this remains
+  mostly experimental. We support `↦` and the connectives of ghost theories in
+  `base_logic/lib`, but support for `own` and custom cameras is minimal and will
+  be improved in future releases.
+* Some initial refactoring prepares Iris for eventually supporting transfinite step-indexing.
+* New resources algebras have been added: `Z`, `max_Z`, `mono_Z`, and `mra` (the
+  monotone resource algebra of https://iris-project.org/pdfs/2021-CPP-monotone-final.pdf)
+
+Iris 4.1 supports Coq 8.16-8.18. Coq 8.13-8.15 are no longer supported.
+
+This release was managed by Ralf Jung, Robbert Krebbers, and Johannes Hostert,
+with contributions from Amin Timany, Arthur Azevedo de Amorim, Armaël Guéneau,
+Benjamin Peters, Dan Frumin, Dorian Lesbre, Ike Mulder, Isaac van Bakel, Jaemin
+Choi, Janine Lohse, Jan-Oliver Kaiser, Jonas Kastberg Hinrichsen, Lennard Gäher,
+Mathias Adam Møller, Michael Sammler, Paolo Giarrusso, Pierre Roux, Rodolphe
+Lepigre, Simcha van Collem, Simon Friis Vindum, Simon Spies, Tej Chajed, Yixuan
+Chen, and Yusuke Matsushita. Thanks a lot to everyone involved!
 
-Coq 8.13, 8.14, and 8.15 are no longer supported.
 
 **Changes in `prelude`:**
 
@@ -53,6 +302,17 @@ Coq 8.13, 8.14, and 8.15 are no longer supported.
 * Add monotone resource algebra, `algebra/mra.v`, to enable reasoning about
   monotonicity with respect to an arbitrary preorder relation: the extension order
   of `mra R` is designed to embed the preorder relation `R`. (by Amin Timany)
+* Rename instances `union_with_proper` → `union_with_ne`,
+  `map_fmap_proper` → `map_fmap_ne`, `map_zip_with_proper` → `map_zip_with_ne`.
+* Rename `dist_option_Forall2` → `option_dist_Forall2`. Add similar lemma
+  `list_dist_Forall2`.
+* Add instances `option_fmap_dist_inj` and `list_fmap_dist_inj`.
+* Rename `list_dist_cons_inv_r` → `cons_dist_eq` and remove
+  `list_dist_cons_inv_l` to be consistent with `cons_equiv_eq` in std++.
+  (If you needed `list_dist_cons_inv_l`, you can apply `symmetry` and
+  then use `cons_dist_eq`.)
+  Add similar lemmas `nil_dist_eq`, `app_dist_eq`, `list_singleton_dist_eq`,
+  `dist_Permutation`.
 
 **Changes in `bi`:**
 
@@ -235,6 +495,9 @@ s/\bbupd_plain\b/bupd_elim/g
 # Logical atomicity (will break Autosubst notation!)
 s/<<</<<\{/g
 s/>>>/\}>>/g
+# option and list
+s/\bdist_option_Forall2\b/option_dist_Forall2/g
+s/\blist_dist_cons_inv_r\b/cons_dist_eq/g
 EOF
 ```
 
@@ -472,7 +735,7 @@ everyone involved!
 
 * Define non-expansive instance for `dom`. This, in particular, makes it
   possible to `iRewrite` below `dom` (even if the `dom` appears in `⌜ _ ⌝`).
-* Generalize the authorative elements of `gmap_view` to be parameterized by a
+* Generalize the authoritative elements of `gmap_view` to be parameterized by a
   [discardable fraction](iris/algebra/dfrac.v) (`dfrac`) instead of a fraction
   (`frac`). Lemmas affected by this have been renamed such that the "frac" in
   their name has been changed into "dfrac". (by Simon Friis Vindum)
@@ -519,7 +782,7 @@ everyone involved!
   propositions that want to support framing are expected to register an
   appropriate instance themselves. HeapLang and gen_heap `↦` still support
   framing, but the other fractional propositions in Iris do not.
-* Strenghten the `Persistent`/`Affine`/`Timeless` results for big ops. Add a `'`
+* Strengthen the `Persistent`/`Affine`/`Timeless` results for big ops. Add a `'`
   to the name of the weaker results, which remain to be used as instances.
 
 **Changes in `heap_lang`:**
@@ -577,7 +840,7 @@ Chajed, and Yusuke Matsushita. Thanks a lot to everyone involved!
 
 **Changes in `algebra`:**
 
-* Generalize the authorative elements of the `view`, `auth` and `gset_bij`
+* Generalize the authoritative elements of the `view`, `auth` and `gset_bij`
   cameras to be parameterized by a [discardable fraction](iris/algebra/dfrac.v)
   (`dfrac`) instead of a fraction (`frac`). Normal fractions are now denoted
   `●{#q} a` and `●V{#q} a`. Lemmas affected by this have been renamed such that
@@ -685,7 +948,7 @@ Chajed, and Yusuke Matsushita. Thanks a lot to everyone involved!
 * Add `ghost_map`, a logic-level library for a `gmap K V` with an authoritative
   view and per-element points-to facts written `k ↪[γ] w`.
 * Generalize the soundness lemma of the base logic `step_fupdN_soundness`.
-  It applies even if invariants stay open accross an arbitrary number of laters.
+  It applies even if invariants stay open across an arbitrary number of laters.
   (by Jacques-Henri Jourdan)
 * Rename those `*G` typeclasses that must be global singletons to `*GS`, and
   their corresponding `preG` class to `GpreS`. Affects `invG`, `irisG`,
@@ -695,7 +958,7 @@ Chajed, and Yusuke Matsushita. Thanks a lot to everyone involved!
 
 * Change definition of weakest precondition to use a variable number of laters
   (i.e., logical steps) for each physical step of the operational semantics,
-  depending on the number of physical steps executed since the begining of the
+  depending on the number of physical steps executed since the beginning of the
   execution of the program. See merge request [!595](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595).
   This implies several API-breaking changes, which can be easily fixed in client
   formalizations in a backward compatible manner as follows:

Makefile

@@ -3,6 +3,12 @@ all: Makefile.coq
 	+@$(MAKE) -f Makefile.coq all
 .PHONY: all
 
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
+
 # Permit local customization
 -include Makefile.local
 

Makefile.coq.local

@@ -4,11 +4,16 @@ NO_TEST:=
 # use MAKE_REF=1 to generate new reference files
 MAKE_REF:=
 
+# Only test reference output on known versions of Coq, to avoid blocking
+# Coq CI when they change the printing a little.
+# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
+COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1)
+
 # Run tests interleaved with main build.  They have to be in the same target for this.
 real-all: style $(if $(NO_TEST),,test)
 
 style: $(VFILES) coq-lint.sh
-# Make sure everything imports the options, and all Instance/Argument/Hint are qualified.
+# Make sure everything imports the options, and some general linting.
 	$(SHOW)"COQLINT"
 	$(HIDE)for FILE in $(VFILES); do \
 	  if ! grep -F -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
@@ -26,8 +31,6 @@ test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
-COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | grep -E '^[0-9]+\.[0-9]+\b' -o)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
@@ -43,17 +46,16 @@ tests/.coqdeps.d: $(TESTFILES)
 # - Either compare the result with the reference file, or move it over the reference file.
 # - Cleanup, and mark as done for make.
 $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
-	$(HIDE)if test -f $*".$(COQ_MINOR_VERSION).ref"; then \
-	    REF=$*".$(COQ_MINOR_VERSION).ref"; \
-	  else \
-	    REF=$*".ref"; \
-	  fi && \
-	  echo "COQTEST$(if $(MAKE_REF), [make ref],) $< (ref: $$REF)" && \
+	$(HIDE)REF=$*".ref" && \
+	  echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref diff ignored]) $< (ref: $$REF)" && \
 	  TMPFILE="$$(mktemp)" && \
 	  unset OCAMLRUNPARAM && \
 	  $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
-	  sed -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
+	  sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
 	  mv "$$TMPFILE".new "$$TMPFILE" && \
-	  $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE") && \
+	  $(if $(COQ_REF),\
+	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
+	    (diff --strip-trailing-cr -u "$$REF" "$$TMPFILE" || true) \
+	  ) && \
 	  rm -f "$$TMPFILE" && \
 	  touch $@

ProofMode.md

-This file has [moved](docs/proof_mode.md).

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.16.1 / 8.17.1 / 8.18.0
+ - Coq 8.19.2 / 8.20.0
  - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
 
 Generally we always aim to support the last two stable Coq releases. Support for

_CoqProject

@@ -10,16 +10,18 @@
 -Q iris_heap_lang iris.heap_lang
 -Q iris_unstable iris.unstable
 -Q iris_deprecated iris.deprecated
+
+# Custom flags (to be kept in sync with the dune file at the root of the repo).
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
-# Disabling warnings about future coercion syntax that requires Coq 8.17
-# (https://github.com/coq/coq/pull/16230)
--arg -w -arg -future-coercion-class-field
-# Some warnings exist only on some Coq versions
--arg -w -arg -unknown-warning
+# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-arg -w -arg -notation-incompatible-prefix
+# We can't do this migration yet until we require Coq 9.0
+-arg -w -arg -deprecated-from-Coq
+-arg -w -arg -deprecated-dirpath-Coq
 
 iris/prelude/options.v
 iris/prelude/prelude.v
@@ -113,6 +115,7 @@ iris/base_logic/lib/mono_nat.v
 iris/base_logic/lib/gset_bij.v
 iris/base_logic/lib/ghost_map.v
 iris/base_logic/lib/later_credits.v
+iris/base_logic/lib/token.v
 iris/program_logic/adequacy.v
 iris/program_logic/lifting.v
 iris/program_logic/weakestpre.v

benchmark/.gitignore

-__pycache__
-build-times*
-gitlab-extract

benchmark/export.py

-#!/usr/bin/env python3
-import argparse, sys, pprint, itertools, subprocess
-import requests
-import parse_log
-
-# read command-line arguments
-parser = argparse.ArgumentParser(description='Export iris-coq build times to grafana')
-parser.add_argument("-f", "--file",
-                    dest="file", required=True,
-                    help="Filename to get the data from.")
-parser.add_argument("-c", "--commits",
-                    dest="commits",
-                    help="Restrict the graph to the given commits.")
-parser.add_argument("-p", "--project",
-                    dest="project", required=True,
-                    help="Project name sent to the server.")
-parser.add_argument("-b", "--branch",
-                    dest="branch", required=True,
-                    help="Branch name sent to the server.")
-parser.add_argument("--config",
-                    dest="config", required=True,
-                    help="The config string.")
-parser.add_argument("-s", "--server",
-                    dest="server", required=True,
-                    help="The server (URL) to send the data to.")
-parser.add_argument("-u", "--user",
-                    dest="user", required=True,
-                    help="Username for HTTP auth.")
-parser.add_argument("--password",
-                    dest="password", required=True,
-                    help="Password for HTTP auth.")
-args = parser.parse_args()
-pp = pprint.PrettyPrinter()
-log_file = sys.stdin if args.file == "-" else open(args.file, "r")
-
-results = parse_log.parse(log_file, parse_times = parse_log.PARSE_RAW)
-if args.commits:
-    commits = set(parse_log.parse_git_commits(args.commits))
-    results = filter(lambda r: r.commit in commits, results)
-results = list(results)
-
-for datapoint in results:
-    times = '\n'.join(datapoint.times)
-    commit = datapoint.commit
-    print("Sending {}...".format(commit), end='')
-    date = subprocess.check_output(['git', 'show', commit, '-s', '--pretty=%cI']).strip().decode('UTF-8')
-    headers = {'X-Project': args.project, 'X-Branch': args.branch, 'X-Commit': commit, 'X-Config': args.config, 'X-Date': date}
-    r = requests.post(args.server+"/build_times", data=times, headers=headers, auth=(args.user, args.password))
-    print(" {}".format(r.text.strip()))
-    r.raise_for_status()

benchmark/gitlab-extract.py

-#!/usr/bin/env python3
-import argparse, pprint, sys, glob, zipfile, subprocess
-import requests
-import parse_log
-
-def last(it):
-    r = None
-    for i in it:
-        r = i
-    return r
-
-def first(it):
-    for i in it:
-        return i
-    return None
-
-def req(path):
-    url = '%s/api/v3/%s' % (args.server, path)
-    r = requests.get(url, headers={'PRIVATE-TOKEN': args.private_token})
-    r.raise_for_status()
-    return r
-
-# read command-line arguments
-parser = argparse.ArgumentParser(description='Extract iris-coq build logs from GitLab')
-parser.add_argument("-t", "--private-token",
-                    dest="private_token", required=True,
-                    help="The private token used to authenticate access.")
-parser.add_argument("-s", "--server",
-                    dest="server", default="https://gitlab.mpi-sws.org/",
-                    help="The GitLab server to contact.")
-parser.add_argument("-p", "--project",
-                    dest="project", default="FP/iris-coq",
-                    help="The name of the project on GitLab.")
-parser.add_argument("-f", "--file",
-                    dest="file", required=True,
-                    help="Filename to store the load in.")
-parser.add_argument("-c", "--commits",
-                    dest="commits",
-                    help="The commits to fetch. Default is everything since the most recent entry in the log file.")
-parser.add_argument("-a", "--artifacts",
-                    dest="artifacts",
-                    help="Location of the artifacts (following GitLab's folder structure).  If not given (which should be the common case), the artifacts will be downloaded from GitLab.")
-parser.add_argument("-b", "--blacklist-branch",
-                    dest="blacklist_branch",
-                    help="Skip the commit if it is contained in the given branch.")
-args = parser.parse_args()
-log_file = sys.stdout if args.file == "-" else open(args.file, "a")
-
-# determine commit, if missing
-if args.commits is None:
-    if args.file == "-":
-        raise Exception("If you do not give explicit commits, you have to give a logfile so that we can determine the missing commits.")
-    last_result = last(parse_log.parse(open(args.file, "r"), parse_times = parse_log.PARSE_NOT))
-    args.commits = "{}..origin/master".format(last_result.commit)
-
-projects = req("projects?per_page=512")
-project = first(filter(lambda p: p['path_with_namespace'] == args.project, projects.json()))
-if project is None:
-    sys.stderr.write("Project not found.\n")
-    sys.exit(1)
-
-BREAK = False
-for commit in parse_log.parse_git_commits(args.commits):
-    if BREAK:
-        break
-    # test to skip the commit
-    if args.blacklist_branch is not None:
-        branches = subprocess.check_output(["git", "branch", "-r", "--contains", commit]).decode("utf-8")
-        if args.blacklist_branch in map(lambda x: x.strip(), branches.split('\n')):
-            continue
-    # Find out more about the commit
-    print("Fetching {}...".format(commit), end='')
-    commit_data = req("/projects/{}/repository/commits/{}".format(project['id'], commit))
-    if commit_data.status_code != 200:
-        raise Exception("Commit not found?")
-    builds = req("/projects/{}/repository/commits/{}/builds".format(project['id'], commit))
-    if builds.status_code != 200:
-        raise Exception("Build not found?")
-    # iterate over builds by decreasing ID, and look for the artifact
-    found_build = False
-    for build in builds.json():
-        if build['status'] in ('created', 'pending', 'running'):
-            # build still not yet done, don't fetch this or any later commit
-            BREAK = True
-            print(" build still in progress, aborting")
-            break
-        if build['status'] != 'success':
-            # build failed or cancelled, skip to next
-            continue
-        # now fetch the build times
-        if args.artifacts:
-            artifact_zip = glob.glob('{}/*/{}/{}/artifacts.zip'.format(args.artifacts, project['id'], build['id']))
-            if not artifact_zip:
-                # no artifact at this build, try another one
-                continue
-            assert len(artifact_zip) == 1, "Found too many artifacts"
-            artifact_zip = artifact_zip[0]
-            with zipfile.ZipFile(artifact_zip) as artifact:
-                with artifact.open('build-time.txt') as build_times:
-                    # Output into log file
-                    log_file.write("# {}\n".format(commit))
-                    log_file.write(build_times.read().decode('UTF-8'))
-                    log_file.flush()
-        else:
-            build_times = requests.get("{}/builds/{}/artifacts/raw/build-time.txt".format(project['web_url'], build['id']))
-            if build_times.status_code != 200:
-                # no artifact at this build, try another one
-                continue
-            # Output in the log file format
-            log_file.write("# {}\n".format(commit))
-            log_file.write(build_times.text)
-            log_file.flush()
-            # don't fetch another build
-            found_build = True
-            print(" success")
-            break
-    if not found_build and not BREAK:
-        print(" found no succeessful build")

benchmark/parse_log.py

-import re, subprocess
-
-class Result:
-    def __init__(self, commit, times):
-        self.commit = commit
-        self.times = times
-
-PARSE_NOT  = 0
-PARSE_RAW  = 1
-PARSE_FULL = 2
-
-def parse(file, parse_times = PARSE_FULL):
-    '''[file] should be a file-like object, an iterator over the lines.
-       yields a list of Result objects.'''
-    commit_re = re.compile("^# ([a-z0-9]+)$")
-    time_re = re.compile("^([a-zA-Z0-9_/-]+) \((real|user): ([0-9.]+).* mem: ([0-9]+) ko\)$")
-    commit = None
-    times = None
-    for line in file:
-        line = line.strip()
-        # next commit?
-        m = commit_re.match(line)
-        if m is not None:
-            # previous commit, if any, is done now
-            if commit is not None:
-                yield Result(commit, times)
-            # start recording next commit
-            commit = m.group(1)
-            if parse_times != PARSE_NOT:
-                times = [] if parse_times == PARSE_RAW else {} # reset the recorded times
-            continue
-        # next file time?
-        m = time_re.match(line)
-        if m is not None:
-            if times is not None:
-                if parse_times == PARSE_RAW:
-                    times.append(line)
-                else:
-                    name = m.group(1)
-                    time = float(m.group(2))
-                    times[name] = time
-            continue
-        # nothing else we know about, ignore
-        print("Ignoring line",line,"(in commit {})".format(commit))
-    # end of file. previous commit, if any, is done now.
-    if commit is not None:
-        yield Result(commit, times)
-
-def parse_git_commits(commits):
-    '''Returns an iterable of SHA1s'''
-    if commits.find('..') >= 0:
-        # a range of commits
-        commits = subprocess.check_output(["git", "rev-list", commits])
-    else:
-        # a single commit
-        commits = subprocess.check_output(["git", "rev-parse", commits])
-    output = commits.decode("utf-8").strip()
-    if not output: # empty output
-        return []
-    return reversed(output.split('\n'))

benchmark/visualize.py

-#!/usr/bin/env python3
-import argparse, sys, pprint, itertools
-import matplotlib.pyplot as plt
-import parse_log
-
-markers = itertools.cycle([(3, 0), (3, 0, 180), (4, 0), (4, 0, 45), (8, 0)])
-
-# read command-line arguments
-parser = argparse.ArgumentParser(description='Visualize iris-coq build times')
-parser.add_argument("-f", "--file",
-                    dest="file", required=True,
-                    help="Filename to get the data from.")
-parser.add_argument("-t", "--timings", nargs='+',
-                    dest="timings",
-                    help="The names of the Coq files (with or without the extension) whose timings should be extracted")
-parser.add_argument("-c", "--commits",
-                    dest="commits",
-                    help="Restrict the graph to the given commits.")
-args = parser.parse_args()
-pp = pprint.PrettyPrinter()
-log_file = sys.stdin if args.file == "-" else open(args.file, "r")
-
-results = parse_log.parse(log_file, parse_times = parse_log.PARSE_FULL)
-if args.commits:
-    commits = set(parse_log.parse_git_commits(args.commits))
-    results = filter(lambda r: r.commit in commits, results)
-results = list(results)
-
-timings = list(map(lambda t: t[:-2] if t.endswith(".v") else t, args.timings))
-for timing in timings:
-    plt.plot(list(map(lambda r: r.times.get(timing), results)), marker=next(markers), markersize=8)
-plt.legend(timings, loc = 'upper left', bbox_to_anchor=(1.05, 1.0))
-plt.xticks(range(len(results)), list(map(lambda r: r.commit[:7], results)), rotation=70)
-plt.subplots_adjust(bottom=0.2, right=0.7) # more space for the commit labels and legend
-
-plt.xlabel('Commit')
-plt.ylabel('Time (s)')
-plt.title('Time to compile files')
-plt.grid(True)
-plt.show()

coq-iris.opam

@@ -27,8 +27,8 @@ tags: [
 ]
 
 depends: [
-  "coq" { (>= "8.16" & < "8.19~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2023-09-21.2.7f6df4fa") | (= "dev") }
+  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq-stdpp" { (= "dev.2024-10-30.1.5297f7c9") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]

docs/dune.md

+Support for the dune build system
+=================================
+
+**NOTE:** in case of problem with the dune build, you can ask @lepigre or
+@Blaisorblade for help.
+
+The library can be built using dune by running `dune build`. Note that `dune`
+needs to be installed separately with `opam install dune`, as it is currently
+not part of the dependencies of the project.
+
+Useful links:
+- [dune documentation](https://dune.readthedocs.io)
+- [coq zulip channel](https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users)
+
+
+Editor support
+--------------
+
+Good dune support in editors is lacking at the moment, but there are tricks you
+can play to make it work.
+
+One option is to configure your editor to invoke the `dune coq top` command
+instead of `coqtop`, but that is not easy to configure.
+
+Another option is to change the `_CoqProject` file to something like:
+```
+-Q iris iris
+-Q _build/default/iris iris
+-Q iris_heap_lang iris.heap_lang
+-Q _build/default/iris_heap_lang iris.heap_lang
+-Q iris_unstable iris.unstable
+-Q _build/default/iris_unstable iris.unstable
+-Q iris_deprecated iris.deprecated
+-Q _build/default/iris_deprecated iris.deprecated
+```
+Note that this includes two bindings for each logical path: a binding to a
+folder in the source tree (where editors will find the `.v` files), and a
+binding to the same folder under `_build/default` (where editors will find
+the corresponding `.vo` files). The binding for a source folder must come
+before the binding for the corresponding build folder, so that editors know
+to jump to source files in the source tree (and not their read-only copy in
+the build folder).
+
+If you do this, you still need to invoke `dune` manually to make sure that the
+dependencies of the file you are stepping through are up-to-date. To build a
+single file, you can do, e.g., `dune build iris/prelude/options.vo`. To build
+only the `iris` folder, you can do `dune build iris`.

docs/editor.md

@@ -5,7 +5,7 @@ If you really want to, you can also avoid having to type unicode characters by
 importing `iris.bi.ascii`.  That enables parsing-only ASCII alternatives to many
 unicode notations. (Feel free to report an issue when you notice that a notation
 is missing.)  The easiest way to learn the ASCII syntax is to
-[read this file](/iris/bi/ascii.v).
+[read this file](../iris/bi/ascii.v).
 Note however that this will make your code harder to read and work on for Iris
 developers that are used to our default unicode notation---generally, our
 recommendation is to use the unicode syntax whenever possible. In particular,
@@ -96,12 +96,12 @@ on the math symbol list, and with some custom aliases for symbols used a lot in
 (mapc (lambda (x)
         (if (cddr x)
             (quail-defrule (cadr x) (car (cddr x)))))
-      (append math-symbol-list-basic math-symbol-list-extended))
+      ; need to reverse since different emacs packages disagree on whether
+      ; the first or last entry should take priority...
+      ; see <https://mattermost.mpi-sws.org/iris/pl/46onxnb3tb8ndg8b6h1z1f7tny> for discussion
+      (reverse (append math-symbol-list-basic math-symbol-list-extended)))
 ```
 
-Finally, set your default input method with `M-x customize-set-value`, setting
-`default-input-method` to `math`.
-
 ### Font Configuration
 
 Even when usable fonts are installed, Emacs tends to pick bad fonts for some

docs/heap_lang.md

@@ -33,7 +33,7 @@ constructor).
 ## Notation
 
 Notation for writing HeapLang terms is defined in
-[`notation.v`](../theories/heap_lang/notation.v).  There are two scopes, `%E` for
+[`notation.v`](../iris_heap_lang/notation.v).  There are two scopes, `%E` for
 expressions and `%V` for values.  For example, `(a, b)%E` is an expression pair
 and `(a, b)%V` a value pair.  The `e` of a `WP e {{ Q }}` is implicitly in `%E`
 scope.
@@ -128,7 +128,7 @@ all of the redexes reduced.)
 Sometimes, it is useful to define a derived notion in HeapLang that involves
 thunks.  For example, the parallel composition `e1 ||| e2` is definable in
 HeapLang, but that requires thunking `e1` and `e2` before passing them to
-`par`. (This is defined in [`par.v`](theories/heap_lang/lib/par.v).)  However,
+`par`. (This is defined in [`par.v`](../iris_heap_lang/lib/par.v).)  However,
 this is somewhat subtle because of the distinction between expression lambdas
 and value lambdas.
 

docs/proof_guide.md

@@ -99,10 +99,9 @@ for further details on `libG` classes).  For example, the STS library is
 parameterized by an STS and assumes that the STS state space is inhabited:
 ```coq
 Class stsG Σ (sts : stsT) := {
-  sts_inG : inG Σ (stsR sts);
+  #[local] sts_inG :: inG Σ (stsR sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
-Local Existing Instance sts_inG.
 ```
 In this case, the `Instance` for this `libG` class has more than just a `subG`
 assumption:

docs/proof_mode.md

@@ -21,7 +21,7 @@ pervasively. These are defined in dedicated sections in this manual.
 
 Many of the tactics below apply to more goals than described in this document
 since the behavior of these tactics can be tuned via instances of the type
-classes in the file [proofmode/classes](iris/proofmode/classes.v). Most notably, many
+classes in the file [proofmode/classes](../iris/proofmode/classes.v). Most notably, many
 of the tactics can be applied when the connective to be introduced or to be eliminated
 appears under a later, an update modality, or in the conclusion of a
 weakest precondition.
@@ -240,18 +240,26 @@ Induction
   + `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction,
   generalizing over the Coq level variables `x1 ... xn`, the hypotheses given by
   the selection pattern `selpat`, and the spatial context as usual.
-- `iInduction x as cpat "IH" "selpat"` : perform induction on
-  the Coq term `x`. The Coq introduction pattern `cpat` is used to name the introduced
-  variables. The induction hypotheses are inserted into the intuitionistic
-  context and given fresh names prefixed `IH`.
-  + `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction,
+- `iInduction x as cpat` : perform induction on the Coq term `x`. The
+  Coq introduction pattern `cpat` is used to name the introduced variables,
+  including the induction hypotheses which are introduced into the proof mode
+  context. Note that induction hypotheses should not be put into string
+  quotation marks `".."`, e.g., use `iInduction n as [|n IH]` to perform
+  induction on a natural number `n`. An implementation caveat is that the names
+  of the induction hypotheses should be fresh in both the Coq context and the
+  proof mode context.
+  + `iInduction x as cpat forall (x1 ... xn) "selpat"` : perform induction,
     generalizing over the Coq level variables `x1 ... xn`, the hypotheses given by
     the selection pattern `selpat`, and the spatial context.
-  + `iInduction x as cpat "IH" using t` : perform induction using the induction
+  + `iInduction x as cpat using t` : perform induction using the induction
     scheme `t`. Common examples of induction schemes are `map_ind`, `set_ind_L`,
     and `gmultiset_ind` for `gmap`, `gset`, and `gmultiset`.
-  + `iInduction x as cpat "IH" using t forall (x1 ... xn) "selpat"` : the above
+  + `iInduction x as cpat using t forall (x1 ... xn) "selpat"` : the above
     variants combined.
+  + `iInduction x as cpat "IH" "selpat"` : ignore the names of the induction
+    hypotheses from `cpat` and call them `IH`, `IH1`, `IH2`, etc. Here "IH" is
+    a string (in string quotation marks). This is *legacy* syntax that might be
+    deprecated in the future. Similar legacy syntax exists for all variants above.
 
 Rewriting / simplification
 --------------------------
@@ -273,6 +281,10 @@ Rewriting / simplification
 - `iSimpl` / `iSimpl in "selpat"` : perform `simpl` on the proof mode
   goal / hypotheses given by the selection pattern `selpat`. This is a
   shorthand for `iEval (simpl)`.
+- `iUnfold xs` / `iUnfold xs in "selpat"` : perform `unfold xs` on the proof
+  mode goal / hypotheses given by the selection pattern `selpat`. This is a
+  shorthand for `iEval (unfold xs)`. Similar to Coq's `unfold`, the argument
+  `xs` should be a comma-separated non-empty list.
 
 Iris
 ----

docs/resource_algebras.md

@@ -99,7 +99,7 @@ To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
 `inG`, you have to assemble a list of functors of all the involved modules,
 and if your proof relies on some singleton (most do, at least indirectly; also
 see the next section), you have to call the respective initialization or
-adequacy lemma.  [For example](tests/one_shot.v):
+adequacy lemma.  [For example](../tests/one_shot.v):
 ```coq
 Section client.
   Context `{!heapGS Σ, !one_shotG Σ, !spawnG Σ}.
@@ -126,14 +126,13 @@ class for the generalized heap module, bundles the usual `inG` assumptions
 together with the `gname`:
 ```coq
 Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heapGpreS_heap : ghost_mapG Σ L V;
+  #[local] gen_heapGpreS_heap :: ghost_mapG Σ L V;
 }.
-Local Existing Instances gen_heapGpreS_heap.
+
 Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
-  gen_heap_inG : gen_heapGpreS L V Σ;
+  #[local] gen_heap_inG :: gen_heapGpreS L V Σ;
   gen_heap_name : gname;
 }.
-Local Existing Instances gen_heap_inG.
 ```
 The trailing `S` here is for "singleton", because the idea is that only one
 instance of `gen_heapGS` ever exists. This is important, since two instances
@@ -142,9 +141,9 @@ would be incompatible with each other.
 
 The `gen_heapGpreS` typeclass (without the singleton data) is relevant for
 initialization, i.e., to create an instance of `gen_heapGS`. This is happening as
-part of [`heap_adequacy`](iris_heap_lang/adequacy.v) using the
+part of [`heap_adequacy`](../iris_heap_lang/adequacy.v) using the
 initialization lemma for `gen_heapGS` from
-[`gen_heap_init`](iris/base_logic/lib/gen_heap.v):
+[`gen_heap_init`](../iris/base_logic/lib/gen_heap.v):
 ```coq
 Lemma gen_heap_init `{gen_heapGpreS L V Σ} σ :
   (|==> ∃ _ : gen_heapGS L V Σ, gen_heap_ctx σ)%I.
@@ -232,9 +231,9 @@ F (X,X⁻) := gmap K (agree (nat * ▶ X))
 To make it convenient to construct such functors and prove their contractivity,
 we provide a number of abstractions:
 
-- [`oFunctor`](iris/algebra/ofe.v): functors from COFEs to OFEs.
-- [`rFunctor`](iris/algebra/cmra.v): functors from COFEs to cameras.
-- [`urFunctor`](iris/algebra/cmra.v): functors from COFEs to unital
+- [`oFunctor`](../iris/algebra/ofe.v): functors from COFEs to OFEs.
+- [`rFunctor`](../iris/algebra/cmra.v): functors from COFEs to cameras.
+- [`urFunctor`](../iris/algebra/cmra.v): functors from COFEs to unital
   cameras.
 
 Besides, there are the classes `oFunctorContractive`, `rFunctorContractive`, and
@@ -283,8 +282,8 @@ Putting it all together, the `libG` typeclass and `libΣ` list of functors for
 your example would look as follows:
 
 ```coq
-Class libG Σ := { lib_inG : inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
-Local Existing Instance lib_inG.
+Class libG Σ :=
+  { #[local] lib_inG :: inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
 
 Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
 Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.