The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

Hello everyone,

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 %H in 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 "[%x ...]" pattern.
• iMod and iModIntro now report an error message for mask mismatches.
• Performance improvements for the proof mode in iFrame in non-affine logics, iPoseProof, and iDestruct (by Paolo G. Giarrusso, Bedrock Systems, and Armaël Guéneau).
• The new ghost_map logic-level library supports a ghost gmap K V with 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, Hai Dang, 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:

• https://gitlab.mpi-sws.org/iris/iris
• https://gitlab.mpi-sws.org/iris/stdpp

If you have any questions, feel free to reply to this email, or join our Iris community chat room.

Best,
The Iris and std++ teams