From 7228c46110b98dae6ef093fd0b95880ab7154e55 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 14 Jul 2020 16:42:10 +0200
Subject: [PATCH] write changelog preamble

---
 CHANGELOG.md | 33 +++++++++++++++++++++++++++++++--
 1 file changed, 31 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 506a86230..9e999683e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -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](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.
+
+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`:**
 
-- 
GitLab