From c63b6a3595aa660cf265e19c74602fb94046e3a7 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 15 Jul 2020 12:54:29 +0200 Subject: [PATCH] edit release notes --- CHANGELOG.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9e999683e..ae6e99067 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,26 +6,26 @@ lemma. ## Iris master This release does not have any outstanding highlights, but contains a large -amount of improvements all over the board. For instance: +number 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. + "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 metric structure, and - still support reasoning about â–·. + 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. -* 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. * 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. -- GitLab