Commit 7228c461 authored by Ralf Jung's avatar Ralf Jung

write changelog preamble

parent fea0c2de
......@@ -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
amount of improvements all over the board. For instance:
* `heap_lang` now supports deallocation as well as better reasoning about
"invariant locations" that are not deallocated and whose value satisfies 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 metric structure, and
still support reasoning about ▷.
* 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.
* The proof mode now provides experimental support for naming pure facts in
intro patterns. See
[iris/string-ident]( for details.
* 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
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment