Commit 6ae02201 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/release' into 'master'

Iris 3.3 changelog summary

See merge request !478
parents 8650d373 c63b6a35
Pipeline #31474 passed with stage
in 22 minutes and 22 seconds
......@@ -5,8 +5,37 @@ lemma.
## Iris master
Coq 8.10, 8.11, and 8.12 are newly supported by this release, and Coq 8.7 and
8.8 are no longer supported.
This release does not have any outstanding highlights, but contains a large
number of improvements all over the board. For instance:
* `heap_lang` now supports deallocation as well as better reasoning about
"invariant locations" (locations that perpetually satisfy some Coq-level
invariant).
* Invariants (`inv N P`) are more flexible, now also supporting splitting
and merging of invariants with respect to separating conjunction.
* Performance of the proofmode for BIs constructed on top of other BIs (e.g.,
`monPred`) was greatly improved, leading to up to 70% speedup in individual
files. As part of this refactoring, the proofmode can now also be instantiated
with entirely "logical" notion of BIs that do not have a (non-trivial) metric
structure, and still support reasoning about ▷.
* The proof mode now provides experimental support for naming pure facts in
intro patterns. See
[iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
* Iris now provides official ASCII notation. We still recommend using the
Unicode notation for better consistency and interoperability with other Iris
libraries, but provide ASCII notation for when Unicode is not an option.
* We removed several coercions, fixing "ambiguous coercion path" warnings and
solving some readability issues.
* Coq 8.10, 8.11, and 8.12 are newly supported by this release, and Coq 8.7 and
8.8 are no longer supported.
Further details are given in the changelog below.
This release of Iris received contributions by Abel Nieto, Amin Timany, Dan
Frumin, Derek Dreyer, Dmitry Khalanskiy, Gregory Malecha, Jacques-Henri Jourdan,
Jonas Kastberg, Jules Jacobs, Matthieu Sozeau, Maxime Dénès, Michael Sammler,
Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Friis Vindum, Simon
Spies, and Tej Chajed. Thanks a lot to everyone involved!
**Changes in `heap_lang`:**
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment