[Iris-Club] Iris 3.3 and std++ 1.4
Ralf Jung
jung at mpi-sws.org
Wed Jul 15 17:53:57 CEST 2020
Hello everyone,
We are pleased to announce the release of Iris 3.3, a concurrent separation
logic framework for Coq. For an overview of the numerous research projects
employing Iris, see <https://iris-project.org/>. Iris 3.3 is accompanied by
std++ 1.4, an extended "standard" library for Coq.
This Iris release does not have any outstanding highlights, but contains a large
number of improvements all over the board. For instance:
* heap_lang (the default programming language shipped with Iris) now supports
deallocation as well as better reasoning about "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 (instances of the "Bunched Implication"
algebra) 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 (non-trivial) metric structure, and still support
reasoning about ▷.
* The proof mode now provides experimental support for naming pure facts in
intro patterns. See <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.
* 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 full changelog at
<https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md>.
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.
For std++, Coq 8.12 is newly supported by this release, and Coq 8.7 is no longer
supported. For further details, see the changelog at
<https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md>. This release
of std++ received contributions by Gregory Malecha, Michael Sammler, Olivier
Laurent, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, sarahzrf, and Tej Chajed.
Thanks a lot to everyone involved!
Both packages will be available in the Coq opam registry shortly. For further
information and installation instructions for Iris and std++, see the respective
project websites:
* https://gitlab.mpi-sws.org/iris/iris
* https://gitlab.mpi-sws.org/iris/stdpp
Best,
The Iris and std++ teams
More information about the Iris-Club
mailing list