# Iris 3.5 and std++ 1.6 released

**URL:** https://discourse.rocq-prover.org/t/iris-3-5-and-std-1-6-released/1486
**Category:** Announcements
**Created:** [November 8, 2021, 1:07pm UTC](https://discourse.rocq-prover.org/t/iris-3-5-and-std-1-6-released/1486 "2021-11-08T13:07:05Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![tchajed](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/tchajed/32/51_2.png) [@tchajed](https://discourse.rocq-prover.org/u/tchajed)
#### Post date: [November 8, 2021, 1:07pm UTC](https://discourse.rocq-prover.org/t/iris-3-5-and-std-1-6-released/1486/1 "2021-11-08T13:07:05Z")

</div>

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/](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](https://gitlab.mpi-sws.org/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](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595) (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](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md#iris-350-2021-11-05)[#iris-350-2021-11-05](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](https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md#std-160-2021-11-05)[#std-160-2021-11-05](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:

- [Iris / Iris · GitLab](https://gitlab.mpi-sws.org/iris/iris)
- [Iris / stdpp · GitLab](https://gitlab.mpi-sws.org/iris/stdpp)

If you have any questions, feel free to post a reply, or join our [Iris community chat room](https://iris-project.org/chat.html).

Best,  
The Iris and std++ teams