.gitignore

@@ -22,3 +22,6 @@ Makefile.coq.conf
 .Makefile.coq.d
 Makefile.package.*
 .Makefile.package.*
+_opam
+_build
+*.install

.gitlab-ci.yml

@@ -5,6 +5,9 @@ stages:
 
 variables:
   CPU_CORES: "10"
+  OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
+  # Avoid needlessly increasing our TCB with native_compute
+  COQEXTRAFLAGS: "-native-compiler no"
 
 .only_branches: &only_branches
   only:
@@ -41,60 +44,49 @@ variables:
 
 ## Build jobs
 
-build-coq.dev:
+# The newest version runs with timing.
+build-coq.8.20.1:
   <<: *template
-  <<: *branches_and_mr
   variables:
-    # Pinning a commit to avoid constant re-builds in MR pipelines
-    COQ_REV: "f16b7c75bcc8651e43ec1f0c8ae6744748665213"
-    OPAM_PINS: "coq-core.dev git git+https://github.com/coq/coq#$COQ_REV   coq-stdlib.dev git git+https://github.com/coq/coq#$COQ_REV   coq.dev git git+https://github.com/coq/coq#$COQ_REV"
-    MANGLE_NAMES: "1"
-
-build-coq.8.14.dev:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.14.dev"
-    MANGLE_NAMES: "1"
-    DENY_WARNINGS: "1"
-
-build-coq.8.13.2:
-  <<: *template
-  interruptible: false
-  variables:
-    OPAM_PINS: "coq version 8.13.2"
+    OPAM_PINS: "coq version 8.20.1"
     DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
     OPAM_PKG: "1"
     DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
     DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
   tags:
   - fp-timing
+  interruptible: false
 
-build-coq.8.12.2:
+# The newest version also runs in MRs, without timing.
+build-coq.8.20.1-mr:
   <<: *template
-  <<: *branches_and_mr
+  <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.12.2"
+    OPAM_PINS: "coq version 8.20.1"
     DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
 
-# Nightly job with a known-to-work Coq version
-# (so failures must be caused by std++)
-trigger-stdpp.dev-coq.8.13.1:
+# Also ensure Dune works.
+build-coq.8.20.1-dune:
   <<: *template
+  <<: *branches_and_mr
   variables:
-    STDPP_REPO: "iris/stdpp"
-    OPAM_PINS: "coq version 8.13.1   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV"
-  except:
-  only:
-  - triggers
-  - schedules
-  - api
+    OPAM_PINS: "coq version 8.20.1   dune version 3.15.2"
+    MAKE_TARGET: "dune"
+
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.19.2:
+  <<: *template
+  <<: *branches_and_mr
+  variables:
+    OPAM_PINS: "coq version 8.19.2"
 
-# Nightly job with latest Coq beta branch
-trigger-stdpp.dev-coq.8.14.dev:
+trigger-stdpp.dev:
   <<: *template
   variables:
     STDPP_REPO: "iris/stdpp"
-    OPAM_PINS: "coq version 8.14.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV"
+    OPAM_PINS: "coq version $NIGHTLY_COQ   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV"
     CI_COQCHK: "1"
   except:
   only:

CHANGELOG.md

@@ -5,11 +5,901 @@ lemma.
 
 ## Iris master
 
-Coq 8.11 is no longer supported in this version of Iris.
+**Changes in `algebra`:**
+
+* Add lemma `ufrac_auth_update_surplus_cancel`.
+* Rename `CsumBot`, `GSetBot`, `CoPsetBot` and `ExclBot` to `*Invalid`.
+* Add `agree_includedN`, `excl_included` and `excl_includedN`.
+
+**Changes in `base_logic`:**
+
+* Add lemmas `own_forall` and `own_and` to reason about universal quantification
+  (`∀ .. own`) and conjunctions (`own .. ∧ own ..`) of ghost ownership. (by
+  Travis Hance)
+  + These rules are derived from the new primitive rule `ownM_forall` (which is
+    proved in the `uPred` model).
+  + Various corollaries for total cmras (which include `ucmra`s) are provided.
+* Add lemma `Some_included_totalI`.
+* Simplify lemma `excl_includedI` to use `=` instead of `match`.
+
+**Changes in `bi`:**
+
+* Merge the two `BiFUpdPlainly` laws `fupd_plainly_mask_empty` and
+  `fupd_plainly_keep_l` into a single law, by generalizing `fupd_plainly_keep_l`
+  so that it subsumes both of them.
+* Change `WP` notation to allow type annotations and (exhaustive) patterns for
+  the return value binder.
+* Rename `bi.lib.fixpoint` module to `bi.lib.fixpoint_mono`.
+* Add `bi.lib.fixpoint_banach` module with lemmas for proving that a `fixpoint`
+  (of a contractive function) is persistent/affine/etc. (with help from William
+  Mansky)
+* Remove the `bool`-valued `stuckness_leb`; use `stuckness_le` (in `Prop`)
+  instead.
+
+**Changes in `proofmode`:**
+
+* Generalize `AsEmpValid` to allow specifying which directions of the bi-implication
+  hold. This allows embedded logics to enable support for `iPoseProof` and `iStartProof`
+  independently. (by Michael Sammler)
+
+**Changes in `heap_lang`:**
+
+* Add `Inhabited lock_name` to `lock` class. (by Daniel Nezamabadi)
+
+**Infrastructure:**
+
+* Use `gmake` (GNU Make) instead of `make` on BSD systems. (by Yiyun Liu)
+
+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
+# "*Bot* RA element rename
+s/\b(Csum|GSet|CoPset|Excl)Bot(\b|_)/\\1Invalid\\2/g
+# bi.lib.fixpoint rename: adjust imports
+s/(From iris.* Require .*|Require iris.*)\bfixpoint\b/\\1fixpoint_mono/g
+EOF
+```
+
+## 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!
+
+
+**Changes in `prelude`:**
+
+* Re-export `stdpp.options` from `iris.prelude.options`. This enables 'light'
+  name mangling, which prefixes auto-generated names with `__`. This only
+  affects developments that explicitly opt-in to following the Iris
+  configuration by importing `iris.prelude.options`.
+
+**Changes in `algebra`:**
+
+* Add (basic) support for `gset` and `gset_disj` cameras to `set_solver`.
+* Rename `sig_{equiv,dist}_alt` into `sig_{equiv,dist}_def` and state these
+  lemmas using `=` instead of `<->`.
+* Add custom entry `dfrac` that can be used for `{dq}` / `□` / `{# q}`
+  annotation of connectives with a discardable fraction.
+* Add an RA on the `Z` type of integers, using addition for `⋅`.
+* Prepare Iris to generalize the type of step-indices. This is a large series of
+  changes; more changes will follow later. More documentation will follow as
+  part of
+  [this merge request](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/888).
+  - Change the definition of `dist_later` to an equivalent definition that is
+    future-proof with respect to general step-indices.
+  - Change the definition of the properties of an `ofe` to be slightly more
+    general and future proof (i.e., change `dist_S` into `dist_lt`).
+  - Adapt `f_contractive` to work with the new definition of `dist_later`.
+    For backwards compatibility for existing developments, the tactic
+    `f_contractive_fin` is provided. It uses the old definition of `dist_later`,
+    now called `dist_later_fin`.
+  - If you need to deal with a `dist_later`/`dist_later_fin` in a manual proof,
+    use the tactic `dist_later_intro`/`dist_later_fin_intro` to introduce it.
+  (by Michael Sammler, Lennard Gäher, and Simon Spies)
+* Add `max_Z` and `mono_Z` cameras.
+* Add `dfrac_valid`.
+* Rename `Some_included_2` to `Some_included_mono`.
+* Consistently use `Some x ≼ Some y` to express the reflexive closure of
+  `x ≼ y`. This changes the statements of some lemmas: `singleton_included`,
+  `local_update_valid0`, `local_update_valid`. Also add various new
+  `Some_included` lemmas to help deal with these assertions.
+* Add hints for `a ≼ a ⋅ _` / `a ≼ _ ⋅ a` / `ε ≼ _` / `_ ≼ CsumBot` /
+  `_ ≼ ExclBot` with cost 0, which means they are used by `done` to finish
+  proofs. (by Ike Mulder)
+* Rename `singleton_mono` to `singleton_included_mono`.
+* Use `Strategy expand` for CMRA/UCMRA coercions and most projections to improve
+  performance of type-checking some large CMRA/OFE types. (by Ike Mulder)
+* 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`:**
+
+* Use `binder` in notations for big ops. This means one can write things such
+  as `[∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝`.
+* Add constructions `bi_tc`/`bi_nsteps` to create the transitive/`n`-step
+  closure of a PROP-level binary relation. (by Simcha van Collem)
+* Make the `unseal` tactic of `monPred` more consistent with `uPred`:
+  + Rename `MonPred.unseal` → `monPred.unseal`
+  + No longer unfold derived BI connectives `<affine>`, `<absorb>` and `◇`.
+  * Make `monPred.unseal` tactic more robust by using types to unfold the right
+    BI projections.
+* Add `unseal` tactic for `siProp`.
+* Add compatibility lemmas for `big_sepL <-> big_sepL2`, `big_sepM <-> big_sepM2`
+  with list/maps of pairs; and `big_sepM <-> big_sepL` via `list_to_map` and
+  `map_to_list`. (by Dorian Lesbre)
+* Make `persistently_True` a bi-entailment; this changes the default `rewrite`
+  direction.
+* Make `BiLaterContractive` a class instead of a notation.
+* Make projections of `Bupd`/`Fupd`/`InternalEq`/`Plainly` operational type
+  classes `Typeclasses Opaque`.
+* Make BI relations (`bi_rtc`, `bi_tc`, `bi_nsteps`) typeclasses opaque (they
+  were accidentally transparent).
+* Make the `P -∗ Q` notation in stdpp_scope (i.e., outside of bi_scope) a
+  shorthand for `⊢ P -∗ Q` rather than `P ⊢ Q`. This means that any BI notation
+  used in stdpp_scope will be sugar for adding a leading `⊢` (`bi_emp_valid`).
+  It also means that `apply` becomes sensitive to the difference between `P ⊢ Q`
+  and `P -∗ Q`, and `rewrite` will only work with lemmas that are explicitly
+  written using `⊢`.
+  When a proof breaks, there are generally 3 options:
+  - Try to find the `-∗` that should be turned into a `⊢` so that things work
+    like before.
+  - Adjust the proof to use proof mode tactics rather than Coq tactics (in
+    particular, replace `apply` by `iApply`).
+  - Add some `apply bi.entails_wand`/`apply bi.wand_entails` to 'convert'
+    between the old and new way of interpreting `P -∗ Q`.
+* Add `auto` hint to introduce the BI version of `↔`.
+* Change `big_sepM2_alt` to use `dom m1 = dom2 m2` instead of
+  `∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)`. The old lemma is still
+  available as `big_sepM2_alt_lookup`.
+* Overhaul `Fractional`/`AsFractional`:
+  - Remove `AsFractional → Fractional` instance.
+  - No longer use `AsFractional P Φ q` backwards, from `Φ` and `q` to `P` -- just
+    use `Φ q` instead.
+  - Remove multiplication instances (that also go from `AsFractional` to
+    `Fractional`, making it very hard to reason about search termination).
+  - Rewrite `frame_fractional` lemma using the new `FrameFractionalQp` typeclass
+    for `Qp` reasoning.
+  - Change statements of `fractional_split`, `fractional_half`, and
+    `fractional_merge` to avoid using `AsFractional` backwards, and only keep
+    the bi-directional versions (remove `fractional_split_1`,
+    `fractional_split_2`, `fractional_half_1`, `fractional_half_2`).
+    `iDestruct`/`iCombine`/`iSplitL`/`iSplitR` should be used instead.
+* Add missing transitivity, symmetry and reflexivity lemmas about the `↔`, `→`,
+  `-∗` and `∗-∗` connectives. (by Ike Mulder)
+* Add `∗-∗` as notation in `stdpp_scope` similar to `-∗`. This means `P ∗-∗ Q`
+  can be directly used as lemma statement, and is syntactic sugar for `⊢ P ∗-∗ Q`.
+* Add `≼` connective (`internal_included`) on the BI level. (by Ike Mulder)
+* Move laws of persistence modality out of `BiMixin` into `BiPersistentlyMixin`.
+* Provide smart constructor `bi_persistently_mixin_discrete` for
+  `BiPersistentlyMixin`: Given a discrete BI that enjoys the existential
+  property, a trivial definition of the persistence modality can be given.
+* Fix `greatest_fixpoint_ne'` accidentally being about the least fixpoint.
+* Add `Plain` instance for `|==> P` when `P` is plain.
+* Rename `bupd_plain` → `bupd_elim`.
+* Change notation for atomic updates and atomic accessors to use `<{ ... }>`
+  instead of `<< ... >>`. This avoids a conflict with Autosubst.
+
+**Changes in `proofmode`:**
+
+* The proof mode introduction patterns "<-" and "->" are considered
+  intuitionistic. This means that tactics such as `iDestruct ... as "->"` will
+  not dispose of hypotheses to perform the rewrite.
+* Remove tactic `iSolveTC` in favor of `tc_solve` in std++.
+* The result of `iCombine` is no longer computed with the `FromSep` typeclass,
+  but with a new `CombineSepAs` typeclass. If you provide custom `FromSep`
+  instances and use the `iCombine` tactic, you will need to define additional
+  `CombineSepAs` instances. This is done in preparation for making `iCombine`
+  combine propositions in ways that are not appropriate for how `FromSep` is used.
+  Note that `FromSep` is still used for determining the new goals when applying
+  the `iSplitL` and `iSplitR` tactics.
+* The `iCombine` tactic now accepts an (optional) 'gives' clause, with which one
+  can learn persistent facts from the combination of two hypotheses. One can
+  register such 'gives' clauses by providing instances of the new
+  `CombineSepGives` typeclass. The 'gives' clause is still experimental;
+  in future versions of Iris it will combine `own` connectives based on the
+  validity rules for cameras.
+* Make sure that `iStartProof` fails with a proper error message on goals with
+  `let`. These `let`s should either be `simpl`ed or introduced into the Coq
+  context using `intros x`, `iIntros (x)`, or `iIntros "%x"`.
+  This can break some proofs that did `iIntros "?"` on a goal of the shape
+  `let ... in P ⊢ Q`.
+* Make `iApply`/`iPoseProof`/`iDestruct` more reliable for lemmas whose
+  statement involves `let`.
+* Remove `string_to_ident`; use `string_to_ident_cps` instead which is in CPS
+  form and hence does not require awful hacks.
+* The `iFrame` tactic now removes some conjunctions and disjunctions with `False`,
+  since additional `MakeOr` and `MakeAnd` instances were provided. If you use these
+  classes, their results may have become more concise.
+* Support n-ary versions of `iIntros`, `iRevert`, `iExists`, `iDestruct`, `iMod`,
+  `iFrame`, `iRevertIntros`, `iPoseProof`, `iInduction`, `iLöb`, `iInv`, and
+  `iAssert`. (by Jan-Oliver Kaiser and Rodolphe Lepigre)
+* Add tactics `ltac1_list_iter` and `ltac1_list_rev_iter` to iterate over
+  lists of `ident`s/`simple intropatterns`/`constr`/etc using Ltac1. See
+  [proofmode/base.v](iris/proofmode/base.v) for documentation on how
+  to use these tactics to convert your own fixed arity tactics to an n-ary
+  variant.
+* Improve the `IntoPure` instance for internal equality. Whenever possible,
+  `a ≡ b` will now be simplified to `a = b` upon introduction into the pure 
+  context. This will break but simplify some existing proofs: 
+  `iIntros (H%leibniz_equiv)` should be replaced by `iIntros (H)`. (by Ike Mulder)
+
+**Changes in `base_logic`:**
+
+* Add `mono_Z` library for monotone non-negative integers.
+  (This has exactly the same lemmas as `mono_nat`. It is useful in cases
+  where one wants to avoid `nat` entirely and use `Z` throughout.)
+* Add `IsExcept0` instance for invariants, allowing you to remove laters of
+  timeless hypotheses when proving an invariant (without an update).
+* Make `uPred.unseal` tactic more robust by using types to unfold the right
+  BI projections.
+* Turn `internal_eq_entails` into a bi-implication.
+* Add lemmas to relate internal/external non-expansiveness and contractiveness.
+* Refactor soundness lemmas: `bupd_plain_soundness` → `bupd_soundness`,
+  `soundness` → `laterN_soundness` + `pure_soundness`; removed
+  `consistency_modal`.
+* Strengthen `cmra_valid_elim` to `✓ a ⊢ ⌜ ✓{0} a ⌝`; make `discrete_valid` a
+  derived law.
+* Remove `frac_validI`. Instead, move to the pure context (with `%` in the proof
+  mode or `uPred.discrete_valid` in manual proofs) and use `frac_valid`.
+
+**Changes in `program_logic`:**
+
+* Change the notation for logically atomic triples: we add support for specifying private (non-atomic) postconditions,
+  and we avoid a notation conflict with Autosubst. The new notation looks as follows:
+  `<<{ ∀∀ x, atomic_pre x }>> code @ ∅ <<{ ∃∃ y, atomic_post x y | z, RET v, non_atomic_post x y z }>>`.
+  To keep the notation without private postcondition consistent, the way the return value is specified changes slightly
+  even when there is no private postcondition:
+  `<<{ ∀∀ x, atomic_pre x }>> code @ ∅ <<{ ∃∃ y, atomic_post x y | RET v }>>`.
+
+**Changes in `heap_lang`:**
+
+* Move operations and lemmas about locations into a module `Loc`.
+* Extend `wp_apply` and `wp_smart_apply` to support immediately introducing the
+  postcondition into the context via `as (x1 ... xn) "ipat1 ... ipatn"`.
+* Add comparison `≤` and `<` for locations. (by Arthur Azevedo de Amorim)
+* Make the generic `lock` interface a typeclass and make sure the lock code
+  does not depend on `Σ`. Code that is generic about lock implementations, or
+  that instantiates that specification, needs adjustment. See
+  [iris_heap_lang/lib/lock.v](iris_heap_lang/lib/lock.v) for documentation on
+  how to work with this specification.
+* Adjust the generic `atomic_heap` interface to follow the same pattern as
+  `lock`.
+* Add a generic `rwlock` interface and a spinning implementation.
+  (by Isaac van Bakel)
+
+**LaTeX changes:**
+
+- Rename `\Alloc` to `\AllocN` and `\Ref` to `\Alloc` for better consistency
+  with the Coq names and to avoid clash with hyperref package.
+
+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
+# iSolveTC
+s/iSolveTC\b/tc_solve/g
+# _alt -> _def
+s/\bsig_equiv_alt\b/sig_equiv_def/g
+s/\bsig_dist_alt\b/sig_dist_def/g
+# Loc
+s/\bloc_add(_assoc|_0|_inj|)\b/Loc.add\1/g
+s/\bfresh_locs(_fresh|)\b/Loc.fresh\1/g
+# unseal
+s/\bMonPred\.unseal\b/monPred\.unseal/g
+# big op
+s/\bbig_sepM2_alt\b/big_sepM2_alt_lookup/g
+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
+```
+
+The following sed script helps adjust LaTeX documents to these changes:
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- *.tex <<EOF
+# Alloc & Ref
+s/\\Alloc\b/\\AllocN/g
+s/\\Ref\b/\\Alloc/g
+EOF
+```
+
+
+## Iris 4.0.0 (2022-08-18)
+
+The highlight of Iris 4.0 is the *later credits* mechanism, which provides a new
+way to eliminate later modalities.
+
+This new mechanism complements the existing techniques of taking program steps,
+exploiting timelessness, and various modality commuting rules. At each program
+step, one obtains a credit `£ 1`, which is an ownable Iris resource. These
+credits don't have to be used at the present step, but can be saved up, and used
+to eliminate laters at any point in the verification using the fancy update
+modality. Later credits are particularly useful in proofs where there is not a
+one-to-one correspondence between program steps and later eliminations, for
+example, logical atomicity proofs. As a consequence, we have been able to
+simplify the definition of logical atomicity by removing the 'laterable'
+mechanism.
+
+The later credit mechanism is described in detail in the
+[ICFP'22 paper](https://plv.mpi-sws.org/later-credits/) and there is a
+[small tutorial](https://gitlab.mpi-sws.org/iris/iris/-/blob/iris-4.0.0/tests/later_credits_paper.v)
+in the Iris repository. The
+[examples](https://gitlab.mpi-sws.org/iris/examples/) repository contains some
+logically atomic case studies that make use of later credits: the counter with a
+backup (Section 4 of the later credits paper), as well as the elimination stack,
+conditional increment, and RDCSS.
+
+Iris 4.0 supports Coq 8.13 - 8.16.
+
+This release was managed by Ralf Jung, Robbert Krebbers, and Lennard Gäher, with
+contributions from Glen Mével, Gregory Malecha, Ike Mulder, Irene Yoon,
+Jan-Oliver Kaiser, Jonas Kastberg Hinrichsen, Lennard Gäher, Michael Sammler,
+Niklas Mück, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Spies,
+and Tej Chajed. Thanks a lot to everyone involved!
+
+**General changes:**
+
+- Rename "unsealing" lemmas from `_eq` to `_unseal`. This particularly
+  affects `envs_entails_eq`, which is commonly used in the definition of
+  custom proof mode tactics. All other unsealing lemmas should be internal, so
+  in principle you should not rely on them.
+- Rename `coq-iris-staging` package to `coq-iris-unstable`, and also change the
+  import path from `iris.staging` to `iris.unstable`.
+
+**Changes in `algebra`:**
+
+* Add some missing algebra functors: `dfrac_agreeRF`, `excl_authURF`, `excl_authRF`,
+  `frac_authURF`, `frac_authRF`, `ufrac_authURF`, `ufrac_authRF`, `max_prefix_listURF`,
+  `max_prefix_listRF`, `mono_listURF`, and `mono_listRF`.
+* Make validy lemmas for `excl_auth` more consistent with `auth`.
+  - Rename `excl_auth_frag_validN_op_1_l` into `excl_auth_frag_op_validN` and
+    `excl_auth_frag_valid_op_1_l` into `excl_auth_frag_op_valid` (similar to
+    `auth_auth_op_valid`), and make them bi-implications.
+  - Add `excl_auth_auth_op_validN` and `excl_auth_auth_op_valid`.
+* Make validy lemmas for `(u)frac_auth` more consistent with `auth`.
+  - Remove unidirectional lemmas with `1` fraction `frac_auth_frag_validN_op_1_l`
+    and `frac_auth_frag_valid_op_1_l`
+  - Add `frac_auth_frag_op_validN` and `frac_auth_frag_op_valid`, which are
+    bi-implications with arbitrary fractions.
+  - Add `ufrac_auth_frag_op_validN` and `ufrac_auth_frag_op_valid`.
+* Remove `mono_list_lb_is_op` instance for `IsOp' (◯ML l) (◯ML l) (◯ML l)`; we
+  don't usually have such instances for duplicable resources and it was added by
+  accident.
+* Rename `pos_op_plus` into `pos_op_add`.
+
+**Changes in `bi`:**
+
+* Generalize `big_op` lemmas that were previously assuming `Absorbing`ness of
+  some assertion: they now take any of (`TCOr`) an `Affine` instance or an
+  `Absorbing` instance. This breaks uses where an `Absorbing` instance was
+  provided without relying on TC search (e.g. in `by apply ...`; a possible fix
+  is `by apply: ...`). (by Glen Mével, Bedrock Systems)
+* Change statement of `affinely_True_emp` to also remove the affinely modality.
+* Rename `absorbingly_True_emp` to `absorbingly_emp_True` and make statement
+  consistent with `affinely_True_emp`: `<absorb> emp ⊣⊢ True`.
+* Change the notation for atomic updates and atomic accessors (`AU`, `AACC`) to
+  swap the quantifiers: the first quantifier is logically an existential, the
+  second a universal, so let's use the appropriate notation. Also use double
+  quantifiers (`∀∀`, `∃∃`) to make it clear that these are not normal
+  quantifiers (the latter change was also applied to logically atomic triples).
+* Add some lemmas to show properties of functions defined via monotonoe fixpoints:
+  `least_fixpoint_affine`, `least_fixpoint_absorbing`,
+  `least_fixpoint_persistent_affine`, `least_fixpoint_persistent_absorbing`,
+  `greatest_fixpoint_absorbing`.
+* Rename `laterN_plus` into `laterN_add`.
+* Remove `make_laterable` from atomic updates. This relies on Iris now having
+  support for later credits (see below).
+* Add `Fractional` and `AsFractional` instances for `embed` such that the
+  embedding of something fractional is also fractional. (by Simon Friis Vindum).
+
+**Changes in `proofmode`:**
+
+* Change `iAssumption` to no longer instantiate evar premises with `False`. This
+  used to occur when the conclusion contains variables that are not in scope of
+  the evar, thus blocking the default behavior of instantiating the premise with
+  the conclusion. The old behavior can be emulated with`iExFalso. iExact "H".`
+* In `iInduction`, support induction schemes that involve `Forall` and
+  `Forall2` (for example, for trees with finite branching).
+* Change `iRevert` of a pure hypothesis to generate a magic wand instead of an
+  implication.
+* Change `of_envs` such that when the persistent context is empty, the
+  persistence modality no longer appears at all. This is a step towards using
+  the proofmode in logics without a persistence modality.
+  The lemma `of_envs_alt` shows equivalence with the old version.
+* Adjust `IntoWand` instances for non-affine BIs: in many cases where
+  `iSpecialize`/`iApply` of an implication previously failed, it will now
+  instead add an `<affine>` modality to the newly generated goal. In some rare
+  cases it might stop working or add an `<affine>` modality where previously
+  none was added.
+
+**Changes in `base_logic`:**
+
+* Make the `inG` instances for `libG` fields local, so they are only used inside
+  the library that defines the `libG`.
+* Add infrastructure for supporting later credits, by adding a resource `£ n`
+  describing ownership of `n` credits that can be eliminated at fancy updates.
+  + To retain backwards compatibility with the interaction laws of fancy updates
+    with the plainly modality (`BiFUpdPlainly`), which are incompatible with
+    later credits, the logic has a new parameter of type `has_lc`, which is
+    either `HasLc` or `HasNoLc`. The parameter is an index of the `invGS_gen`
+    typeclass; the old `invGS` is an alias for `invGS_gen HasLc` so that
+    developments default to having later credits available. Libraries that want
+    to be generic over whether credits are available or not, and proofs that
+    need `BiFUpdPlainly`, need to be changed to use `invGS_gen` rather than
+    `invGS`.
+  + The core soundness lemma `step_fupdN_soundness_gen` similarly takes a `has_lc`
+    parameter to control how the logic is supposed to be instantiated. The lemma
+    always generates credits, but they cannot be used in any meaningful way unless
+    `HasLc` is picked.
+* Add discardable fractions `dfrac` to `saved_anything_own`, `saved_prop_own`,
+  and `saved_pred_own`, so they can be updated. The previous persistent versions
+  can be recovered with the fraction `DfracDiscarded`. Allocation lemmas now take
+  a `dq` parameter to define the initial fraction.
+* Remove an unused fraction argument to `dfrac_valid_discarded`.
+
+**Changes in `program_logic`:**
+
+* The definition of the weakest precondition has been changed to generate later credits
+  (see `base_logic`) for each step:
+  + The member `num_laters_per_step` of the `irisGS` class now also determines the number
+    of later credits that are generated: `S (num_laters_per_step ns)` if `ns` steps
+    have been taken.
+  + The weakest precondition offers credits after a `prim_step` has been proven.
+  + All lifting lemmas have been altered to provide credits.
+    `wp_lift_step_fupdN` provides `S (num_laters_per_step ns)` credits, while all other
+    lemmas always provide one credit.
+* In line with the support for later credits (see `base_logic`), `irisGS_gen`
+  now also has a `has_lc` parameter and the adequacy statements have been
+  changed to account for that:
+  + The lemma `twp_total` (total adequacy) provides `irisGS_gen HasNoLc`. Clients
+    of the adequacy proof will need to make sure to be either generic over the
+    choice of `has_lc` or explicitly opt-out of later credits.
+  + The adequacy lemmas for the partial WP, in particular `wp_adequacy`,
+    `wp_strong_adequacy` and `wp_invariance`, are now available in two flavors:
+    the old names generate `irisGS` (a short-hand for `irisGS_gen HasLc`); new
+    lemmas with a `_gen` suffix leave the choice of `has_lc` to the user.
+  + The parameter for the stuckness bit `s` in `wp_strong_adequacy{_lc, _no_lc}` has
+    moved up and is now universally quantified in the lemma instead of being existentially
+    quantified at the Iris-level. For clients that already previously quantified over `s`
+    at the Coq level, the only required change should be to remove the instantiation
+    of the existential quantifier.
+
+**Changes in `iris_heap_lang`:**
+
+* Change the `num_laters_per_step` of `heap_lang` to `λ n, n`, signifying that
+  each step of the weakest precondition strips `n` laters, where `n` is the
+  number of steps taken so far. This number is tied to ghost state in the state
+  interpretation, which is exposed, updated, and used with new lemmas
+  `wp_lb_init`, `wp_lb_update`, and `wp_step_fupdN_lb`. (by Jonas Kastberg Hinrichsen)
+* Make pattern argument of `wp_pure` tactic optional (defaults to wildcard
+  pattern, matching all redexes).
+* In line with the support for later credits (see `base_logic`), the tactic
+  `wp_pure` now takes an optional parameter `credit:"H"` which generates a
+  hypothesis `H` for a single later credit `£ 1` that can be eliminated using
+  `lc_fupd_elim_later`.
+  The typeclass `heapGS_gen` now takes an additional `has_lc` parameter, and
+  `heapGS` is a short-hand for `heapGS_gen HasLc`. The adequacy statements for
+  HeapLang have been changed accordingly:
+  + `heap_adequacy` provides `heapGS`, thus enabling the use of later credits.
+    This precludes usage of the laws in `BiFUpdPlainly` in the HeapLang instance of Iris.
+  + `heap_total` provides `heapGS_gen HasNoLc`.
+
+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
+# excl_auth
+s/\bexcl_auth_frag_validN_op_1_l\b/excl_auth_frag_op_validN/g
+s/\bexcl_auth_frag_valid_op_1_l\b/excl_auth_frag_op_valid/g
+# staging → unstable
+s/\biris\.staging\b/iris.unstable/g
+# plus → add
+s/\blaterN_plus\b/laterN_add/g
+s/\bpos_op_plus\b/pos_op_add/g
+EOF
+```
+
+## Iris 3.6.0 (2022-01-22)
+
+The highlights and most notable changes of this release are:
+
+* Coq 8.15 is now supported, while Coq 8.13 and Coq 8.14 remain supported.
+  Coq 8.12 is no longer supported.
+* Support for discardable fractions (`dfrac`) has been added to `gmap_view`
+  authoritative elements, and to the `mono_nat` library. See below for other
+  `dfrac`-related changes.
+* A new `mono_list` algebra provides monotonically growing lists with an
+  exclusive authoritative element and persistent prefix witnesses. See
+  `iris/algebra/lib/mono_list.v` for details. An experimental logic-level
+  library wrapping the algebra is available at
+  `iris_staging/base_logic/mono_list.v`; if you use it, please give feedback on
+  the tracking issue
+  [iris/iris#439](https://gitlab.mpi-sws.org/iris/iris/-/issues/439).
+
+This release was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with
+contributions from Dan Frumin, Jonas Kastberg Hinrichsen, Lennard Gäher,
+Matthieu Sozeau, Michael Sammler, Paolo G. Giarrusso, Ralf Jung, Robbert
+Krebbers, Simon Friis Vindum, Tej Chajed, and Vincent Siles. Thanks a lot to
+everyone involved!
+
+**Changes in `algebra`**
+
+* Define non-expansive instance for `dom`. This, in particular, makes it
+  possible to `iRewrite` below `dom` (even if the `dom` appears in `⌜ _ ⌝`).
+* 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)
+* Change `ufrac_auth` notation to not use curly braces, since these fractions do
+  not behave like regular fractions (and cannot be made `dfrac`).
+  Old: `●U{q} a`, `◯U{q} b`; new: `●U_q a`, `◯U_q b`.
+* Equip `frac_agree` with support for `dfrac` and rename it to `dfrac_agree`.
+  The old `to_frac_agree` and its lemmas still exist, except that the
+  `frac_agree_op_valid` lemmas are made bi-directional.
+* Rename typeclass instance `Later_inj` -> `Next_inj`.
+* Remove `view_auth_frac_op`, `auth_auth_frac_op`, `gmap_view_auth_frac_op`; the
+  corresponding `dfrac` lemmas can be used instead (together with `dfrac_op_own`
+  if needed).
+* Equip `mono_nat` algebra with support for `dfrac`, make API more consistent,
+  and add notation for algebra elements. See `iris/algebra/lib/mono_nat.v` for
+  details. This affects some existing terms and lemmas:
+  - `mono_nat_auth` now takes a `dfrac`, but the recommendation is to port to the notation.
+  - `mono_nat_lb_op`: direction of equality is swapped.
+  - `mono_nat_auth_frac_op`, `mono_nat_auth_frac_op_valid`,
+    `mono_nat_auth_frac_valid`, `mono_nat_both_frac_valid`: use `dfrac` variant
+    instead.
+* Add `mono_list` algebra for monotonically growing lists with an exclusive
+  authoritative element and persistent prefix witnesses. See
+  `iris/algebra/lib/mono_list.v` for details.
+
+**Changes in `bi`:**
+
+* Rename `least_fixpoint_ind` into `least_fixpoint_iter`,
+  rename `greatest_fixpoint_coind` into `greatest_fixpoint_coiter`,
+  rename `least_fixpoint_strong_ind` into `least_fixpoint_ind`,
+  add lemmas `least_fixpoint_{ind_wf, ne', strong_mono}`, and
+  add lemmas `greatest_fixpoint_{coind, paco, ne', strong_mono}`.
+* Move `persistently_forall_2` (`∀ <pers> ⊢ <pers> ∀`) out of the BI interface
+  into a new typeclass, `BiPersistentlyForall`. The BI interface instead just
+  demands the equivalent property for conjunction (`(<pers> P) ∧ (<pers> Q) ⊢
+  <pers> (P ∧ Q)`). This enables the IPM to support logics where the
+  persistently modality is defined with an existential quantifier. This also
+  necessitates removing `persistently_impl_plainly` from `BiPlainly` into a new
+  typeclass `BiPersistentlyImplPlainly`.
+  Proofs that are generic in `PROP` might have to add those new classes as
+  assumptions to remain compatible, and code that instantiates the BI interface
+  needs to provide instances for the new classes.
+* Make `frame_fractional` not an instance any more; instead fractional
+  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.
+* 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`:**
+
+* The `is_closed_expr` predicate is formulated in terms of a
+  set of binders (as opposed to a list of binders).
+
+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
+# least/greatest fixpoint renames
+s/\bleast_fixpoint_ind\b/least_fixpoint_iter/g
+s/\bgreatest_fixpoint_coind\b/greatest_fixpoint_coiter/g
+s/\bleast_fixpoint_strong_ind\b/least_fixpoint_ind/g
+# gmap_view renames from frac to dfrac
+s/\bgmap_view_(auth|both)_frac_(op_invN|op_inv|op_inv_L|valid|op_validN|op_valid|op_valid_L)\b/gmap_view_\1_dfrac_\2/g
+s/\bgmap_view_persist\b/gmap_view_frag_persist/g
+# frac_agree with dfrac
+s/\bfrac_agreeR\b/dfrac_agreeR/g
+EOF
+```
+
+## Iris 3.5.0 (2021-11-05)
+
+The highlights and most notable changes of this release are:
+
+* Coq 8.14 is now supported, while Coq 8.12 and Coq 8.13 remain supported.
+* The proof mode now has native support for pure names `%H` in intro patterns,
+  without installing
+  [iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident). If you had
+  the plugin installed, to migrate simply uninstall the plugin and stop
+  importing it.
+* The proof mode now supports destructing existentials with the `"[%x ...]"`
+  pattern.
+* `iMod` and `iModIntro` now report an error message for mask mismatches.
+* Performance improvements for the proof mode in `iFrame` in non-affine
+  logics, `iPoseProof`, and `iDestruct` (by Paolo G. Giarrusso, Bedrock Systems,
+  and Armaël Guéneau).
+* The new `ghost_map` logic-level library supports a ghost `gmap K V` with an
+  authoritative view and per-element points-to facts written `k ↪[γ] w`.
+* Weakest preconditions now support a flexible number of laters per
+  physical step of the operational semantics. See merge request
+  [!585](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595) (by
+  Jacques-Henri Jourdan and Yusuke Matsushita).
+* HeapLang now has an atomic `Xchg` (exchange) operation (by Simon Hudon,
+  Google).
+
+This release was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with
+contributions from Amin Timany, Armaël Guéneau, Dan Frumin, Dmitry Khalanskiy,
+Hoang-Hai Dang, Jacques-Henri Jourdan, Lennard Gäher, Michael Sammler, Paolo G.
+Giarrusso, Ralf Jung, Robbert Krebbers, Simon Friis Vindum, Simon Hudon, Tej
+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
@@ -68,6 +958,13 @@ Coq 8.11 is no longer supported in this version of Iris.
   by combining the embeddings of `PROP1` into `PROP2` and `PROP2` into `PROP3`.
   This construct is *not* declared as an instance to avoid TC search divergence.
   (by Hai Dang, BedRock Systems)
+* Improve notation printing around magic wands, view shifts, `WP`, Texan
+  triples, and logically atomic triples.
+* Slight change to the `AACC` notation for atomic accessors (which is usually
+  only printed, not parsed): added a `,` before `ABORT`, for consistency with `COMM`.
+* Add the lemmas `big_sepM_impl_strong` and `big_sepM_impl_dom_subseteq` that
+  generalize the existing `big_sepM_impl` lemma. (by Simon Friis Vindum)
+* Add new instance `fractional_big_sepL2`. (by Paolo G. Giarrusso, BedRock Systems)
 
 **Changes in `proofmode`:**
 
@@ -87,6 +984,15 @@ Coq 8.11 is no longer supported in this version of Iris.
   [iris/proofmode/frame_instances.v](iris/proofmode/frame_instances.v) and
   https://coq.inria.fr/refman/addendum/type-classes.html#coq:cmd.Instance. (by
   Paolo G. Giarrusso, BedRock Systems)
+* Rename the main entry point module for the proofmode from
+  `iris.proofmode.tactics` to `iris.proofmode.proofmode`. Under normal
+  circumstances, this should be the only proofmode file you need to import.
+* Improve performance of the `iIntoEmpValid` tactic used by `iPoseProof`,
+  especially in the case of large goals and lemmas with many forall quantifiers.
+  (by Armaël Guéneau)
+* Improve performance of the `iDestruct` tactic, by using user-provided names
+  more eagerly in order to avoid later calls to `iRename`.
+  (by Armaël Guéneau)
 
 **Changes in `bi`:**
 
@@ -101,7 +1007,7 @@ Coq 8.11 is no longer supported in this version of Iris.
 * 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`,
@@ -111,7 +1017,7 @@ Coq 8.11 is no longer supported in this version of Iris.
 
 * 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:
@@ -126,6 +1032,7 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Remove `wp_frame_wand_l`; add `wp_frame_wand` as more symmetric replacement.
 * Swap the polarity of the mask in logically atomic triples, so that it matches
   regular `WP` masks.
+* Rename `iris_invG` to `iris_invGS`.
 
 **Changes in `heap_lang`:**
 
@@ -152,6 +1059,11 @@ s/\bbupd_forall\b/bupd_plain_forall/g
 # "global singleton" rename
 s/\b(inv|iris|(gen|inv)_heap|(Gen|Inv)Heap|proph_map|ProphMap|[oO]wnP|[hH]eap)G\b/\1GS/g
 s/\b([iI]nv|iris|(gen|inv)_heap|(Gen|Inv)Heap|proph_map|ProphMap|[oO]wnP|[hH]eap)PreG\b/\1GpreS/g
+# iris.proofmode.tactics → iris.proofmode.proofmode
+s/\bproofmode\.tactics\b/proofmode.proofmode/
+s/(From +iris\.proofmode +Require +(Import|Export).*)\btactics\b/\1proofmode/
+# iris_invG → iris_invGS
+s/\biris_invG\b/iris_invGS/g
 EOF
 ```
 

CONTRIBUTING.md

@@ -42,6 +42,9 @@ requests are easier to review, and will typically be merged more quickly
 (because it avoids blocking the whole merge request on a single
 discussion).
 
+Please follow the coding style laid out in our [style
+guide](docs/style_guide.md).
+
 ## How to update the std++ dependency
 
 * Do the change in std++, push it.

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,18 +4,23 @@ 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 ! fgrep -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
+	  if ! grep -F -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
 	  ./coq-lint.sh "$$FILE" || exit 1; \
 	done
 # Make sure main Iris does not import other Iris packages.
-	$(HIDE)if egrep 'iris\.(heap_lang|deprecated|staging)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
+	$(HIDE)if grep -E 'iris\.(heap_lang|deprecated|unstable)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
 .PHONY: style
 
 # the test suite
@@ -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)" | egrep '^[0-9]+\.[0-9]+\b' -o)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
@@ -37,21 +40,22 @@ tests/.coqdeps.d: $(TESTFILES)
 # Main test script (comments out-of-line because macOS otherwise barfs?!?)
 # - Determine reference file (`REF`).
 # - Print user-visible status line.
+# - unset env vars that change Coq's output
 # - Dump Coq output into a temporary file.
 # - Run `sed -i` on that file in a way that works on macOS.
 # - 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 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 -u "$$REF" "$$TMPFILE") && \
+	  $(if $(COQ_REF),\
+	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
+	    true \
+	  ) && \
 	  rm -f "$$TMPFILE" && \
 	  touch $@

ProofMode.md

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

README.md

-# IRIS COQ DEVELOPMENT [[coqdoc]](https://plv.mpi-sws.org/coqdoc/iris/)
+# Iris Coq Development [[coqdoc]](https://plv.mpi-sws.org/coqdoc/iris/)
 
 This is the Coq development of the [Iris Project](http://iris-project.org),
 which includes [MoSeL](http://iris-project.org/mosel/), a general proof mode
@@ -30,13 +30,15 @@ Importing Iris has some side effects as the library sets some global options.
 
 This version is known to compile with:
 
- - Coq 8.12.2 / 8.13.2
+ - Coq 8.19.2 / 8.20.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).
+Generally we always aim to support the last two stable Coq releases. Support for
+older versions will be dropped when it is convenient.
+
+If you need to work with older versions of Coq, you can check out the
+[tags](https://gitlab.mpi-sws.org/iris/iris/-/tags) for old Iris releases that
+still support them.
 
 ### Working *with* Iris
 
@@ -65,7 +67,7 @@ We do not guarantee backwards-compatibility, so upgrading Iris may break your
 Iris-using developments.  If you want to be notified of breaking changes, please
 let us know your account name on the
 [MPI-SWS GitLab](https://gitlab.mpi-sws.org/) so we can add you to the
-notification group.  Note that this excludes the "staging" and "deprecated"
+notification group.  Note that this excludes the "unstable" and "deprecated"
 packages (see below).
 
 #### Use of Iris in submitted artifacts
@@ -124,7 +126,7 @@ modules in separate folders.
     constructions within this language, e.g., parallel composition.
     For more examples of using Iris and heap_lang, have a look at the
     [Iris Examples](https://gitlab.mpi-sws.org/iris/examples).
-* The [iris_staging](iris_staging) package contains libraries that are not yet
+* The [iris_unstable](iris_unstable) package contains libraries that are not yet
   ready for inclusion in Iris proper. For each library, there is a corresponding
   "tracking issue" in the Iris issue tracker (also linked from the library
   itself) which tracks the work that still needs to be done before moving the
@@ -138,6 +140,9 @@ modules in separate folders.
   infrastructure. These modules are not installed by `make install`, and should
   not be imported.
 
+Note that the unstable and deprecated packages are not released, so they only
+exist in the development version of Iris.
+
 ## Case Studies
 
 The following is a (probably incomplete) list of case studies that use Iris, and
@@ -160,6 +165,7 @@ that should be compatible with this version:
 
 Getting along with Iris in Coq:
 
+* The coding style is documented in the [style guide](docs/style_guide.md).
 * Iris proof patterns and conventions are documented in the
   [proof guide](docs/proof_guide.md).
 * Various notions of equality and logical entailment in Iris and their Coq
@@ -172,10 +178,9 @@ Getting along with Iris in Coq:
 
 Contacting the developers:
 
-* Discussion about the Iris Coq development happens on the mailing list
-  [iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club)
-  and in the [Iris Chat](https://iris-project.org/chat.html).  This is also the
-  right place to ask questions.
+* Discussion about the Iris Coq development happens in the [Iris
+  Chat](https://iris-project.org/chat.html). This is also the right place to ask
+  questions.
 * If you want to report a bug, please use the
   [issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which requires
   an MPI-SWS GitLab account. The [chat page](https://iris-project.org/chat.html)

_CoqProject

@@ -8,13 +8,20 @@
 -Q iris/base_logic iris.base_logic
 -Q iris/program_logic iris.program_logic
 -Q iris_heap_lang iris.heap_lang
--Q iris_staging iris.staging
+-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
+# 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
@@ -47,12 +54,15 @@ iris/algebra/ufrac.v
 iris/algebra/reservation_map.v
 iris/algebra/dyn_reservation_map.v
 iris/algebra/max_prefix_list.v
+iris/algebra/mra.v
 iris/algebra/lib/excl_auth.v
 iris/algebra/lib/frac_auth.v
 iris/algebra/lib/ufrac_auth.v
-iris/algebra/lib/frac_agree.v
+iris/algebra/lib/dfrac_agree.v
 iris/algebra/lib/gmap_view.v
 iris/algebra/lib/mono_nat.v
+iris/algebra/lib/mono_Z.v
+iris/algebra/lib/mono_list.v
 iris/algebra/lib/gset_bij.v
 iris/si_logic/siprop.v
 iris/si_logic/bi.v
@@ -72,8 +82,10 @@ iris/bi/monpred.v
 iris/bi/embedding.v
 iris/bi/weakestpre.v
 iris/bi/telescopes.v
+iris/bi/lib/cmra.v
 iris/bi/lib/counterexamples.v
-iris/bi/lib/fixpoint.v
+iris/bi/lib/fixpoint_mono.v
+iris/bi/lib/fixpoint_banach.v
 iris/bi/lib/fractional.v
 iris/bi/lib/laterable.v
 iris/bi/lib/atomic.v
@@ -103,6 +115,8 @@ iris/base_logic/lib/ghost_var.v
 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
@@ -130,16 +144,19 @@ iris/proofmode/sel_patterns.v
 iris/proofmode/tactics.v
 iris/proofmode/notation.v
 iris/proofmode/classes.v
+iris/proofmode/classes_make.v
 iris/proofmode/class_instances.v
 iris/proofmode/class_instances_later.v
 iris/proofmode/class_instances_updates.v
 iris/proofmode/class_instances_embedding.v
 iris/proofmode/class_instances_plainly.v
 iris/proofmode/class_instances_internal_eq.v
-iris/proofmode/frame_instances.v
+iris/proofmode/class_instances_frame.v
+iris/proofmode/class_instances_make.v
 iris/proofmode/monpred.v
 iris/proofmode/modalities.v
 iris/proofmode/modality_instances.v
+iris/proofmode/proofmode.v
 
 iris_heap_lang/locations.v
 iris_heap_lang/lang.v
@@ -158,8 +175,10 @@ iris_heap_lang/lib/spawn.v
 iris_heap_lang/lib/par.v
 iris_heap_lang/lib/assert.v
 iris_heap_lang/lib/lock.v
+iris_heap_lang/lib/rw_lock.v
 iris_heap_lang/lib/spin_lock.v
 iris_heap_lang/lib/ticket_lock.v
+iris_heap_lang/lib/rw_spin_lock.v
 iris_heap_lang/lib/nondet_bool.v
 iris_heap_lang/lib/lazy_coin.v
 iris_heap_lang/lib/clairvoyant_coin.v
@@ -169,13 +188,12 @@ iris_heap_lang/lib/increment.v
 iris_heap_lang/lib/diverge.v
 iris_heap_lang/lib/arith.v
 iris_heap_lang/lib/array.v
+iris_heap_lang/lib/logatom_lock.v
 
-iris_staging/algebra/list.v
-iris_staging/algebra/mono_list.v
-iris_staging/base_logic/algebra.v
-iris_staging/base_logic/mono_list.v
-iris_staging/heap_lang/interpreter.v
-iris_staging/algebra/monotone.v
+iris_unstable/algebra/list.v
+iris_unstable/base_logic/algebra.v
+iris_unstable/base_logic/mono_list.v
+iris_unstable/heap_lang/interpreter.v
 
 iris_deprecated/base_logic/auth.v
 iris_deprecated/base_logic/sts.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-heap-lang.opam

@@ -9,8 +9,12 @@ version: "dev"
 
 synopsis: "The canonical example language for Iris"
 description: """
-This package provides the iris.heap_lang Coq module.
+This package defines HeapLang, a concurrent lambda calculus with references, and
+uses Iris to build a program logic for HeapLang programs.
 """
+tags: [
+  "logpath:iris.heap_lang"
+]
 
 depends: [
   "coq-iris" {= version}

coq-iris-staging.opam → coq-iris-unstable.opam

@@ -18,5 +18,5 @@ depends: [
   "coq-iris-heap-lang" {= version}
 ]
 
-build: ["./make-package" "iris_staging" "-j%{jobs}%"]
-install: ["./make-package" "iris_staging" "install"]
+build: ["./make-package" "iris_unstable" "-j%{jobs}%"]
+install: ["./make-package" "iris_unstable" "install"]

coq-iris.opam

@@ -9,13 +9,26 @@ version: "dev"
 
 synopsis: "A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
 description: """
-This package provides the following Coq modules:
-iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_logic, iris.program_logic.
+Iris is a framework for reasoning about the safety of concurrent programs using
+concurrent separation logic. It can be used to develop a program logic, for
+defining logical relations, and for reasoning about type systems, among other
+applications. This package includes the base logic, Iris Proof Mode (IPM) /
+MoSeL, and a general language-independent program logic; see coq-iris-heap-lang
+for an instantiation of the program logic to a particular programming language.
 """
+tags: [
+  "logpath:iris.prelude"
+  "logpath:iris.algebra"
+  "logpath:iris.si_logic"
+  "logpath:iris.bi"
+  "logpath:iris.proofmode"
+  "logpath:iris.base_logic"
+  "logpath:iris.program_logic"
+]
 
 depends: [
-  "coq" { (>= "8.12" & < "8.15~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2021-07-26.0.e263eb10") | (= "dev") }
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
+  "coq-stdpp" { (= "dev.2025-02-26.0.d2e8771d") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]

coq-lint.sh

@@ -4,7 +4,7 @@ set -e
 
 FILE="$1"
 
-if egrep -n '^\s*((Existing\s+|Program\s+)Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|Opaque|Transparent)\b' "$FILE"; then
+if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold|Rewrite)|(Open|Close)\s+Scope|Opaque|Transparent|Typeclasses (Opaque|Transparent))\b' "$FILE"; then
     echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
     echo "Please add 'Global' or 'Local' as appropriate."
     echo

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](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/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
@@ -125,140 +125,65 @@ results in a decent choice for the symbols used in Iris:
 (set-fontset-font t nil (font-spec :name "Symbola"))
 ```
 
+### Automated Indentation
+
+The default indentation configuration of company-coq is not compatible with the Iris syntax.
+As a result, automatic indentation will indent lines incorrectly.
+
+To solve some of these indentation errors you can add the following line to your Emacs
+initialisation file:
+```
+(setq coq-smie-user-tokens
+   '(("," . ":=")
+	("∗" . "->")
+	("-∗" . "->")
+	("∗-∗" . "->")
+	("==∗" . "->")
+	("=∗" . "->") 			;; Hack to match ={E1,E2}=∗
+	("|==>" . ":=")
+	("⊢" . "->")
+	("⊣⊢" . "->")
+	("↔" . "->")
+	("←" . "<-")
+	("→" . "->")
+	("=" . "->")
+	("==" . "->")
+	("/\\" . "->")
+	("⋅" . "->")
+	(":>" . ":=")
+	("by" . "now")
+	("forall" . "now")              ;; NB: this breaks current ∀ indentation.
+   ))
+```
+This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the
+closely related Coq symbols (e.g. `->`).
+Note that `->` is used in many places, as its indentation behaviour is:
+```
+  P ->
+  Q
+```
+This is the indentation behaviour is what we want, e.g. for `∗`:
+```
+  P ∗
+  Q
+```
+Note that this configuration has some caveats.
+Notably, the change to `forall` (which gives good behavior to e.g.
+`iInduction xs as [|x xs IHxs] forall (ys).`), now gives the following indentation
+behavior to universal quantification:
+```
+  ∀ x,
+  P x
+```
+This is not what we want; the second line should be indented by 2 spaces.
+
 ## CoqIDE 8.9 and earlier on Linux (ibus-m17n)
 
 On Linux with old versions of CoqIDE you can use the Intelligent
 Input Bus (IBus) framework to input Unicode symbols. First, install `ibus-m17n`
 via your system's package manager. Next, create a file `~/.m17n.d/coq.mim` to
 configure an input method based on the math symbol list, and with some custom
-aliases for symbols used a lot in Iris:
-
-```
-;; Usage: copy to ~/.m17n.d/coq.mim
-
-(input-method t coq)
-(description "Input method for Coq")
-(title "Coq")
-
-(map (trans
-
-;; Standard LaTeX math notations
-  ("\\forall"         "∀")
-  ("\\exists"         "∃")
-  ("\\lam"            "λ")
-  ("\\not"            "¬")
-  ("\\/"              "∨")
-  ("/\\"              "∧")
-  ("->"               "→")
-  ("<->"              "↔")
-  ("\\<-"             "←") ;; we add a backslash because the plain <- is used for the rewrite tactic
-  ("\\=="             "≡")
-  ("\\/=="            "≢")
-  ("/="               "≠")
-  ("<="               "≤")
-  ("\\in"             "∈")
-  ("\\notin"          "∉")
-  ("\\cup"            "∪")
-  ("\\cap"            "∩")
-  ("\\setminus"       "∖")
-  ("\\subset"         "⊂")
-  ("\\subseteq"       "⊆")
-  ("\\sqsubseteq"     "⊑")
-  ("\\sqsubseteq"     "⊑")
-  ("\\notsubseteq"    "⊈")
-  ("\\meet"           "⊓")
-  ("\\join"           "⊔")
-  ("\\top"            "⊤")
-  ("\\bottom"         "⊥")
-  ("\\vdash"          "⊢")
-  ("\\dashv"          "⊣")
-  ("\\Vdash"          "⊨")
-  ("\\infty"          "∞")
-  ("\\comp"           "∘")
-  ("\\prf"            "↾")
-  ("\\bind"           "≫=")
-  ("\\mapsto"         "↦")
-  ("\\hookrightarrow" "↪")
-  ("\\uparrow"        "↑")
-
-;; Iris specific
-  ("\\fun"            "λ")
-  ("\\mult"           "⋅")
-  ("\\ent"            "⊢")
-  ("\\valid"          "✓")
-  ("\\diamond"        "◇")
-  ("\\box"            "□")
-  ("\\bbox"           "■")
-  ("\\later"          "▷")
-  ("\\pred"           "φ")
-  ("\\and"            "∧")
-  ("\\or"             "∨")
-  ("\\comp"           "∘")
-  ("\\ccomp"          "◎")
-  ("\\all"            "∀")
-  ("\\ex"             "∃")
-  ("\\to"             "→")
-  ("\\sep"            "∗")
-  ("\\lc"             "⌜")
-  ("\\rc"             "⌝")
-  ("\\Lc"             "⎡")
-  ("\\Rc"             "⎤")
-  ("\\empty"          "∅")
-  ("\\Lam"            "Λ")
-  ("\\Sig"            "Σ")
-  ("\\-"              "∖")
-  ("\\aa"             "●")
-  ("\\af"             "◯")
-  ("\\auth"           "●")
-  ("\\frag"           "◯")
-  ("\\iff"            "↔")
-  ("\\gname"          "γ")
-  ("\\incl"           "≼")
-  ("\\latert"         "▶")
-  ("\\update"         "⇝")
-  ("\\bind"           "≫=")
-
-;; accents (for iLöb)
-  ("\\\"o" "ö")
-
-;; subscripts and superscripts
-  ("^^+" "⁺") ("__+" "₊") ("^^-" "⁻")
-  ("__0" "₀") ("__1" "₁") ("__2" "₂") ("__3" "₃") ("__4" "₄")
-  ("__5" "₅") ("__6" "₆") ("__7" "₇") ("__8" "₈") ("__9" "₉")
-
-  ("__a" "ₐ") ("__e" "ₑ") ("__h" "ₕ") ("__i" "ᵢ") ("__k" "ₖ")
-  ("__l" "ₗ") ("__m" "ₘ") ("__n" "ₙ") ("__o" "ₒ") ("__p" "ₚ")
-  ("__r" "ᵣ") ("__s" "ₛ") ("__t" "ₜ") ("__u" "ᵤ") ("__v" "ᵥ") ("__x" "ₓ")
-
-;; Greek alphabet
-  ("\\Alpha"  "Α")   ("\\alpha"  "α")
-  ("\\Beta"   "Β")   ("\\beta"   "β")
-  ("\\Gamma"  "Γ")   ("\\gamma"  "γ")
-  ("\\Delta"  "Δ")   ("\\delta"  "δ")
-  ("\\Epsilon"  "Ε") ("\\epsilon"  "ε")
-  ("\\Zeta"   "Ζ")   ("\\zeta"   "ζ")
-  ("\\Eta"  "Η")     ("\\eta"  "η")
-  ("\\Theta"  "Θ")   ("\\theta"  "θ")
-  ("\\Iota"   "Ι")   ("\\iota"   "ι")
-  ("\\Kappa"  "Κ")   ("\\kappa"  "κ")
-  ("\\Lamda"  "Λ")   ("\\lamda"  "λ")
-  ("\\Lambda"   "Λ") ("\\lambda"   "λ")
-  ("\\Mu"   "Μ")     ("\\mu"   "μ")
-  ("\\Nu"   "Ν")     ("\\nu"   "ν")
-  ("\\Xi"   "Ξ")     ("\\xi"   "ξ")
-  ("\\Omicron"  "Ο") ("\\omicron"  "ο")
-  ("\\Pi"   "Π")     ("\\pi"   "π")
-  ("\\Rho"  "Ρ")     ("\\rho"  "ρ")
-  ("\\Sigma"  "Σ")   ("\\sigma"  "σ")
-  ("\\Tau"  "Τ")     ("\\tau"  "τ")
-  ("\\Upsilon"  "Υ") ("\\upsilon"  "υ")
-  ("\\Phi"  "Φ")     ("\\phi"  "φ")
-  ("\\Chi"  "Χ")     ("\\chi"  "χ")
-  ("\\Psi"  "Ψ")     ("\\psi"  "ψ")
-  ("\\Omega"  "Ω")   ("\\omega"  "ω")
-))
-(state (init (trans)))
-```
+aliases for symbols used a lot in Iris as defined [here](ibus).
 
 To use this input method, you should:
 
@@ -373,7 +298,7 @@ commands and keyboard shortcuts.
 To use unicode you need a font that supports all the symbols, such as [Fira
 Code](https://github.com/tonsky/FiraCode/wiki/Installing). Download and install
 the font, and in VS Code press `Cmd ,` or `Ctrl ,` to go to the settings, search
-for "font", and use "FiraCode-Retina" as the font-family and optionally enable
+for "font", and use "FiraCode-Retina" on macOS or "Fira Code Retina" on Linux as the font-family and optionally enable
 ligatures.
 
 ### Unicode input setup
@@ -383,185 +308,85 @@ extension](https://marketplace.visualstudio.com/items?itemName=mr-konn.generic-i
 To insert a symbol, type the code for a symbol such as `\to` and then press
 `Space` or `Tab`. To enable Iris unicode input support, open your user settings,
 press `Cmd ,` or `Ctrl ,`, type "generic-input-methods.input-methods", and then
-click on "Edit in settings.json" and add the following:
+click on "Edit in settings.json" and add the contents of [this file](vscode).
+
+## Vim
+
+The [Coqtail](https://github.com/whonore/coqtail) plugin can be used to develop Coq code in `vim` (install it with your favorite plugin manager).
+Follow the installation instructions in Coqtail's README to setup your keybinds and find out about its usage.
+
+### Unicode support
+For Unicode support, make sure that your terminal emulator supports Unicode and configure it to use a font with Unicode support.
+
+For entering Unicode symbols, one option is the plugin [latex-unicoder](https://github.com/joom/latex-unicoder.vim).
+Install it with your favorite plugin manager.
+To enter a Unicode symbol, hit `C-l` in normal or insert mode. For more details on the usage, see its README.
 
+latex-unicoder comes with a large set of pre-configured symbols known from LaTeX, but you can also add your own by adding (and adapting) the following to your `.vimrc`:
 ```
-  "generic-input-methods.input-methods": [
-        {
-            "name": "Iris Math",
-            "commandName": "text.math",
-            "languages": [
-                "coq"
-            ],
-            "triggers": [
-                "\\"
-            ],
-            "dictionary": [
-                // Standard LaTeX math notations
-                { "label": "forall", "body": "∀", "description": "∀" },
-                { "label": "exists", "body": "∃", "description": "∃" },
-                { "label": "lam", "body": "λ", "description": "λ" },
-                { "label": "not", "body": "¬", "description": "¬" },
-                { "label": "->", "body": "→", "description": "→" },
-                { "label": "<->", "body": "↔", "description": "↔" },
-                { "label": "<-", "body": "←", "description": "←" },
-                { "label": "==", "body": "≡", "description": "≡" },
-                { "label": "/==", "body": "≢", "description": "≢" },
-                { "label": "/=", "body": "≠", "description": "≠" },
-                { "label": "neq", "body": "≠", "description": "≠" },
-                { "label": "nequiv", "body": "≢", "description": "≢" },
-                { "label": "<=", "body": "≤", "description": "≤" },
-                { "label": "leq", "body": "≤", "description": "≤" },
-                { "label": "in", "body": "∈", "description": "∈" },
-                { "label": "notin", "body": "∉", "description": "∉" },
-                { "label": "cup", "body": "∪", "description": "∪" },
-                { "label": "cap", "body": "∩", "description": "∩" },
-                { "label": "setminus", "body": "∖", "description": "∖" },
-                { "label": "subset", "body": "⊂", "description": "⊂" },
-                { "label": "subseteq", "body": "⊆", "description": "⊆" },
-                { "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
-                { "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
-                { "label": "notsubseteq", "body": "⊈", "description": "⊈" },
-                { "label": "meet", "body": "⊓", "description": "⊓" },
-                { "label": "join", "body": "⊔", "description": "⊔" },
-                { "label": "top", "body": "⊤", "description": "⊤" },
-                { "label": "bottom", "body": "⊥", "description": "⊥" },
-                { "label": "vdash", "body": "⊢", "description": "⊢" },
-                { "label": "|-", "body": "⊢", "description": "⊢" },
-                { "label": "dashv", "body": "⊣", "description": "⊣" },
-                { "label": "Vdash", "body": "⊨", "description": "⊨" },
-                { "label": "infty", "body": "∞", "description": "∞" },
-                { "label": "comp", "body": "∘", "description": "∘" },
-                { "label": "prf", "body": "↾", "description": "↾" },
-                { "label": "bind", "body": "≫=", "description": "≫=" },
-                { "label": "mapsto", "body": "↦", "description": "↦" },
-                { "label": "hookrightarrow", "body": "↪", "description": "↪" },
-                { "label": "uparrow", "body": "↑", "description": "↑" },
-
-                // Iris specific
-                { "label": "fun", "body": "λ", "description": "λ" },
-                { "label": "mult", "body": "⋅", "description": "⋅" },
-                { "label": "ent", "body": "⊢", "description": "⊢" },
-                { "label": "valid", "body": "✓", "description": "✓" },
-                { "label": "diamond", "body": "◇", "description": "◇" },
-                { "label": "box", "body": "□", "description": "□" },
-                { "label": "bbox", "body": "■", "description": "■" },
-                { "label": "later", "body": "▷", "description": "▷" },
-                { "label": "pred", "body": "φ", "description": "φ" },
-                { "label": "and", "body": "∧", "description": "∧" },
-                { "label": "or", "body": "∨", "description": "∨" },
-                { "label": "comp", "body": "∘", "description": "∘" },
-                { "label": "ccomp", "body": "◎", "description": "◎" },
-                { "label": "all", "body": "∀", "description": "∀" },
-                { "label": "ex", "body": "∃", "description": "∃" },
-                { "label": "to", "body": "→", "description": "→" },
-                { "label": "sep", "body": "∗", "description": "∗" },
-                { "label": "star", "body": "∗", "description": "∗" },
-                { "label": "lc", "body": "⌜", "description": "⌜" },
-                { "label": "rc", "body": "⌝", "description": "⌝" },
-                { "label": "Lc", "body": "⎡", "description": "⎡" },
-                { "label": "Rc", "body": "⎤", "description": "⎤" },
-                { "label": "empty", "body": "∅", "description": "∅" },
-                { "label": "Lam", "body": "Λ", "description": "Λ" },
-                { "label": "Sig", "body": "Σ", "description": "Σ" },
-                { "label": "-", "body": "∖", "description": "∖" },
-                { "label": "aa", "body": "●", "description": "●" },
-                { "label": "af", "body": "◯", "description": "◯" },
-                { "label": "auth", "body": "●", "description": "●" },
-                { "label": "frag", "body": "◯", "description": "◯" },
-                { "label": "iff", "body": "↔", "description": "↔" },
-                { "label": "gname", "body": "γ", "description": "γ" },
-                { "label": "incl", "body": "≼", "description": "≼" },
-                { "label": "latert", "body": "▶", "description": "▶" },
-                { "label": "update", "body": "⇝", "description": "⇝" },
-                { "label": "bind", "body": "≫=", "description": "≫=" },
-
-                // accents (for iLöb)
-                { "label": "\"o", "body": "ö", "description": "ö" },
-
-                // subscripts and superscripts
-                { "label": "^^+", "body": "⁺", "description": "⁺" },
-                { "label": "__+", "body": "₊", "description": "₊" },
-                { "label": "^^-", "body": "⁻", "description": "⁻" },
-                { "label": "__0", "body": "₀", "description": "₀" },
-                { "label": "__1", "body": "₁", "description": "₁" },
-                { "label": "__2", "body": "₂", "description": "₂" },
-                { "label": "__3", "body": "₃", "description": "₃" },
-                { "label": "__4", "body": "₄", "description": "₄" },
-                { "label": "__5", "body": "₅", "description": "₅" },
-                { "label": "__6", "body": "₆", "description": "₆" },
-                { "label": "__7", "body": "₇", "description": "₇" },
-                { "label": "__8", "body": "₈", "description": "₈" },
-                { "label": "__9", "body": "₉", "description": "₉" },
-                { "label": "__a", "body": "ₐ", "description": "ₐ" },
-                { "label": "__e", "body": "ₑ", "description": "ₑ" },
-                { "label": "__h", "body": "ₕ", "description": "ₕ" },
-                { "label": "__i", "body": "ᵢ", "description": "ᵢ" },
-                { "label": "__k", "body": "ₖ", "description": "ₖ" },
-                { "label": "__l", "body": "ₗ", "description": "ₗ" },
-                { "label": "__m", "body": "ₘ", "description": "ₘ" },
-                { "label": "__n", "body": "ₙ", "description": "ₙ" },
-                { "label": "__o", "body": "ₒ", "description": "ₒ" },
-                { "label": "__p", "body": "ₚ", "description": "ₚ" },
-                { "label": "__r", "body": "ᵣ", "description": "ᵣ" },
-                { "label": "__s", "body": "ₛ", "description": "ₛ" },
-                { "label": "__t", "body": "ₜ", "description": "ₜ" },
-                { "label": "__u", "body": "ᵤ", "description": "ᵤ" },
-                { "label": "__v", "body": "ᵥ", "description": "ᵥ" },
-                { "label": "__x", "body": "ₓ", "description": "ₓ" },
-
-                // Greek alphabet
-                { "label": "Alpha", "body": "Α", "description": "Α" },
-                { "label": "alpha", "body": "α", "description": "α" },
-                { "label": "Beta", "body": "Β", "description": "Β" },
-                { "label": "beta", "body": "β", "description": "β" },
-                { "label": "Gamma", "body": "Γ", "description": "Γ" },
-                { "label": "gamma", "body": "γ", "description": "γ" },
-                { "label": "Delta", "body": "Δ", "description": "Δ" },
-                { "label": "delta", "body": "δ", "description": "δ" },
-                { "label": "Epsilon", "body": "Ε", "description": "Ε" },
-                { "label": "epsilon", "body": "ε", "description": "ε" },
-                { "label": "Zeta", "body": "Ζ", "description": "Ζ" },
-                { "label": "zeta", "body": "ζ", "description": "ζ" },
-                { "label": "Eta", "body": "Η", "description": "Η" },
-                { "label": "eta", "body": "η", "description": "η" },
-                { "label": "Theta", "body": "Θ", "description": "Θ" },
-                { "label": "theta", "body": "θ", "description": "θ" },
-                { "label": "Iota", "body": "Ι", "description": "Ι" },
-                { "label": "iota", "body": "ι", "description": "ι" },
-                { "label": "Kappa", "body": "Κ", "description": "Κ" },
-                { "label": "kappa", "body": "κ", "description": "κ" },
-                { "label": "Lamda", "body": "Λ", "description": "Λ" },
-                { "label": "lamda", "body": "λ", "description": "λ" },
-                { "label": "Lambda", "body": "Λ", "description": "Λ" },
-                { "label": "lambda", "body": "λ", "description": "λ" },
-                { "label": "Mu", "body": "Μ", "description": "Μ" },
-                { "label": "mu", "body": "μ", "description": "μ" },
-                { "label": "Nu", "body": "Ν", "description": "Ν" },
-                { "label": "nu", "body": "ν", "description": "ν" },
-                { "label": "Xi", "body": "Ξ", "description": "Ξ" },
-                { "label": "xi", "body": "ξ", "description": "ξ" },
-                { "label": "Omicron", "body": "Ο", "description": "Ο" },
-                { "label": "omicron", "body": "ο", "description": "ο" },
-                { "label": "Pi", "body": "Π", "description": "Π" },
-                { "label": "pi", "body": "π", "description": "π" },
-                { "label": "Rho", "body": "Ρ", "description": "Ρ" },
-                { "label": "rho", "body": "ρ", "description": "ρ" },
-                { "label": "Sigma", "body": "Σ", "description": "Σ" },
-                { "label": "sigma", "body": "σ", "description": "σ" },
-                { "label": "Tau", "body": "Τ", "description": "Τ" },
-                { "label": "tau", "body": "τ", "description": "τ" },
-                { "label": "Upsilon", "body": "Υ", "description": "Υ" },
-                { "label": "upsilon", "body": "υ", "description": "υ" },
-                { "label": "Phi", "body": "Φ", "description": "Φ" },
-                { "label": "phi", "body": "φ", "description": "φ" },
-                { "label": "Chi", "body": "Χ", "description": "Χ" },
-                { "label": "chi", "body": "χ", "description": "χ" },
-                { "label": "Psi", "body": "Ψ", "description": "Ψ" },
-                { "label": "psi", "body": "ψ", "description": "ψ" },
-                { "label": "Omega", "body": "Ω", "description": "Ω" },
-                { "label": "omega", "body": "ω", "description": "ω" }
-            ]
-        }
-    ]
+let g:unicode_map = {
+  \ "\\fun"     :   "λ",
+  \ "\\mult"    :   "⋅",
+  \ "\\ent"     :   "⊢",
+  \ "\\valid"   :   "✓",
+  \ "\\diamond" :   "◇",
+  \ "\\box"     :   "□",
+  \ "\\bbox"   	:   "■",
+  \ "\\later"  	:   "▷",
+  \ "\\pred"   	:   "φ",
+  \ "\\and"    	:   "∧",
+  \ "\\or"     	:   "∨",
+  \ "\\comp"   	:   "∘",
+  \ "\\ccomp"  	:   "◎",
+  \ "\\all"    	:   "∀",
+  \ "\\ex"     	:   "∃",
+  \ "\\to"     	:   "→",
+  \ "\\sep"    	:   "∗",
+  \ "\\lc"     	:   "⌜",
+  \ "\\rc"     	:   "⌝",
+  \ "\\Lc"     	:   "⎡",
+  \ "\\Rc"     	:   "⎤",
+  \ "\\lam"    	:   "λ",
+  \ "\\empty"  	:   "∅",
+  \ "\\Lam"    	:   "Λ",
+  \ "\\Sig"    	:   "Σ",
+  \ "\\-"      	:   "∖",
+  \ "\\aa"     	:   "●",
+  \ "\\af"     	:   "◯",
+  \ "\\auth"   	:   "●",
+  \ "\\frag"   	:   "◯",
+  \ "\\iff"    	:   "↔",
+  \ "\\gname"  	:   "γ",
+  \ "\\incl"   	:   "≼",
+  \ "\\latert" 	:   "▶",
+  \ "\\update" 	:   "⇝",
+  \ "\\\"o"     :   "ö",
+  \ "_a"        :   "ₐ",
+  \ "_e"        :   "ₑ",
+  \ "_h"        :   "ₕ",
+  \ "_i"        :   "ᵢ",
+  \ "_k"        :   "ₖ",
+  \ "_l"        :   "ₗ",
+  \ "_m"        :   "ₘ",
+  \ "_n"        :   "ₙ",
+  \ "_o"        :   "ₒ",
+  \ "_p"        :   "ₚ",
+  \ "_r"        :   "ᵣ",
+  \ "_s"        :   "ₛ",
+  \ "_t"        :   "ₜ",
+  \ "_u"        :   "ᵤ",
+  \ "_v"        :   "ᵥ",
+  \ "_x"        :   "ₓ",
+\ }
 ```
+
+
+Alternatively, you can use snippets using [UltiSnips](https://github.com/SirVer/ultisnips).
+
+Install it with your favorite plugin manager, and register a completion key in your configuration:
+```
+let g:UltiSnipsExpandTrigger="<c-l>"
+```
+To insert a unicode character, type its trigger word, such as `\forall` or `->`, and then press `<c-l>` while still in insert mode.
+
+To register most common unicode characters, put [this file](vim_ultisnips) either at `~/.vim/UltiSnips/coq_unicode.snippets` or `~/.config/nvim/UltiSnips/coq_unicode.snippets`, depending on your preferred variant of Vim.