We are happy to announce the release of Iris 3.5 and std++ 1.6. Iris is a concurrent separation logic framework for Coq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Coq.
The highlights and most notable changes of Iris 3.5 are:
- Coq 8.14 is now supported, while Coq 8.12 and Coq 8.13 remain supported.
- The proof mode now has native support for pure names
%Hin intro patterns, without installing iris/string-ident. If you had the plugin installed, to migrate simply uninstall the plugin and stop importing it.
- The proof mode now supports destructing existentials with the
iModIntronow report an error message for mask mismatches.
- Performance improvements for the proof mode in
iFramein non-affine logics,
iDestruct(by Paolo G. Giarrusso, Bedrock Systems, and Armaël Guéneau).
- The new
ghost_maplogic-level library supports a ghost
gmap K Vwith an authoritative view and per-element points-to facts written
k ↪[γ] w.
- Weakest preconditions now support a flexible number of laters per physical step of the operational semantics. See merge request !585 (by Jacques-Henri Jourdan and Yusuke Matsushita).
- HeapLang now has an atomic
Xchg(exchange) operation (by Simon Hudon, Google).
Further details are given in the changelog at https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md#iris-350-2021-11-05.
This release was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with contributions from Amin Timany, Armaël Guéneau, Dan Frumin, Dmitry Khalanskiy, Hoang-Hai Dang, Jacques-Henri Jourdan, Lennard Gäher, Michael Sammler, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Friis Vindum, Simon Hudon, Tej Chajed, and Yusuke Matsushita. Thanks a lot to everyone involved!
For std++, Coq 8.14 is newly supported, while Coq 8.10 to 8.13 remain supported.
This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with contributions from Alix Trieu, Andrej Dudenhefner, Dan Frumin, Fengmin Zhu, Hoang-Hai Dang, Jan, Lennard Gäher, Michael Sammler, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Friis Vindum, Simon Gregersen, and Tej Chajed. Thanks a lot to everyone involved!
For further details, see the full changelog at https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md#std-160-2021-11-05.
Both packages are available in the Coq opam registry. For further information and installation instructions for Iris and std++, see the respective project websites:
If you have any questions, feel free to post a reply, or join our Iris community chat room.
The Iris and std++ teams