From 48787e36af2ccb900063fcfcf7a84486643eae72 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 18 May 2020 13:36:08 +0200 Subject: [PATCH] changelog --- CHANGELOG.md | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1c852bbbd..b31cefd06 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,20 +7,28 @@ Coq development, but not every API-breaking change is listed. Changes marked **Changes in the theory of Iris itself:** -* [#] Redefine invariants as "semantic invariants" so that they support +* [#] Redefined invariants as "semantic invariants" so that they support splitting and other forms of weakening. * Updated the strong variant of the opening lemma for cancellable invariants to match that of regular invariants, where you can pick the mask at a later time. **Changes in program logic:** -* In the axiomatization of ectx languages we replace the axiom of positivity of +* In the axiomatization of ectx languages we replaced the axiom of positivity of context composition with an axiom that says if `fill K e` takes a head step, then either `K` is the empty evaluation context or `e` is a value. * Added a library for "invariant locations": heap locations that will not be deallocated (i.e., they are GC-managed) and satisfy some pure, Coq-level invariant. See `iris.base_logic.lib.gen_inv_heap` for details. +**Changes in heap_lang:** + +* Added a fraction to the heap_lang `array` assertion. +* Added array_copy library for copying and cloning arrays. +* Added the ghost state for "invariant locations" to `heapG`. This affects the + statement of `heap_adequacy`, which is now responsible for initializing the + "invariant locations" invariant. + **Changes in Coq:** * Added support for Coq 8.10 and Coq 8.11; dropped support for Coq 8.7 and Coq 8.8. @@ -170,11 +178,6 @@ s/\blist_singletonM_included\b/list_singleton_included/g ' $(find theories -name "*.v") ``` -**Changes in heap_lang:** - -* Added a fraction to the heap_lang `array` assertion. -* Added array_copy library for copying and cloning arrays. - ## Iris 3.2.0 (released 2019-08-29) The highlight of this release is the completely re-engineered interactive proof -- GitLab