Hi everyone,
We are happy to announce the release of Iris 4.4 and std++ 1.12. Iris is a concurrent separation logic framework for Rocq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Rocq.
The main new Iris features are support for transfinite step-indexing for resource algebras, and new proof rules for reasoning about propositions of the form ∀ .. own and own .. ∧ own ... Otherwise, these releases mostly include quality of life improvements.
For Iris, the supported Rocq versions are 8.19 - 9.0, while std++ also supports version 8.18.
For further details, see the full changelog of Iris and std++.
This release was managed by Jesper Bengtson, Ralf Jung and Robbert Krebbers.
std++ received contributions from Andres Erbsen, Kimaya Bedarkar, Marijn van Wezel, Michael Sammler, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, Rudy Peterson, and Marijn van Wezel.
Iris received contributions from Benjamin Peters, Daniel Nezamabadi, Ike Mulder, Isaac van Bakel, Jan-Oliver Kaiser, Janggun Lee, Johannes Hostert, Lennard Gäher, Michael Sammler, Paolo G. Giarrusso, Pierre Roux, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, Sanjit Bhat, Tej Chajed, Travis Hance, William Mansky, Yixuan Chen, Yiyun Liu, Yusuke Matsushita, Rudy Peterson, and Thomas Somers.
Thanks a lot to everyone involved!
Both packages are available in the Rocq 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 reply to this email, or join our Iris community chat room: Iris Chat Room: Iris Chat Room.
We are also happy to announce iris-contrib (Iris / iris-contrib · GitLab) on behalf of the iris-contrib maintainers:
Iris-contrib is meant to collect community additions to Iris and std++, especially in the form of utility lemmas. As such, it is the ideal destination for the collected lemmas in everyone’s util.v files. 
And if you need a lemma that you cannot find in Iris or std++, maybe someone has already proved it in iris-contrib!
Iris-contrib has low requirements for MRs (see the README) – as long as it compiles and you put your lemmas in sensible places, you should be good. The plan for popular additions is to eventually upstream them to Iris or std++. We hope that iris-contrib will also be a useful staging ground for trying out and discussing additions.
Iris-contrib is maintained by Vincent Lafeychine and Lennard Gäher. We aim to ensure compatibility with Iris master and that iris-contrib always builds, but provide no further stability guarantees.
Best,
The Iris and std++ teams