From abc98e0aff0b66a0312befa168e2051091de2924 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 2 Jul 2018 10:58:26 +0200 Subject: [PATCH] CHANGELOG --- CHANGELOG.md | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5a38620fc..8bba3a075 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,12 +11,33 @@ Changes in and extensions of the theory: the quantification over the next states and the later modality. This makes it possible to prove more powerful lifting lemmas: The new versions feature an "update that takes a step". +* [#] Weaken the semantics of CAS in heap_lang to be efficiently implementable: + CAS may only be used to compare "unboxed" values that can be represented in a + single machine word. * [#] Add weakest preconditions for total program correctness. * [#] "(Potentially) stuck" weakest preconditions are no longer considered experimental. Changes in Coq: +* An all-new generalized proofmode that abstracts away from Iris! The proofmode + can now be used with non-step-indexed and even non-affine (i.e., linear) + logics. TODO: Add reference to paper. Developments instantiating the + proofmode typeclasses may need significant changes. For developments just + using the proofmode tactics, porting should not be too much effort. Notable + things to port are: + - All the BI laws moved from the `uPred` module to the `bi` module. For + example, `uPred.later_equivI` became `bi.later_equivI`. + - Big-ops are automatically imported, imports of `iris.base_logic.big_op` have + to be removed. + - The ⊢ notation can sometimes infer different (but convertible) terms when + seraching for the BI to use, which (due to Coq limitations) can lead to + failing rewrites, in particular when rewriting at function types. +* The `iInv` tactic can now be used without the second argument (the name for + the closing update). It will then instead add the obligation to close the + invariant to the goal. +* Improved pretty-printing of Iris connectives (in particular WP and fancy + updates) when Coq has to line-wrap the output. * Rename `timelessP` -> `timeless` (projection of the `Timeless` class) * The CMRA axiom `cmra_extend` is now stated in `Type`, using `sigT` instead of in `Prop` using `exists`. This makes it possible to define the function space -- GitLab