[Iris-Club] Iris 3.2 and std++ 1.2.1

[Ralf Jung]

Dear Iris-club,

We are pleased to announce the release of Iris 3.2 and std++ 1.2.1.

The highlight of the new Iris release is the completely re-engineered
interactive proof mode. Not only did many tactics become more powerful; the
entire proof mode can now be used not just for Iris but also for other
separation logics satisfying the proof mode interface (e.g., [Iron] and
[GPFSL]). Also see the [accompanying paper][MoSeL].

[Iron]: https://iris-project.org/iron/
[GPFSL]: https://gitlab.mpi-sws.org/iris/gpfsl/
[MoSeL]: https://iris-project.org/mosel/

Beyond that, the Iris program logic gained the ability to reason about
potentially stuck programs, and a significantly strengthened adequacy theorem
that unifies the three previously separately presented theorems. There are now
also Hoare triples for total program correctness (but with very limited support
for invariants) and logical atomicity.

And finally, our example language HeapLang was made more realistic
(Compare-and-set got replaced by compare-exchange and limited to only compare
values that can actually be compared atomically) and more powerful, with added
support for arrays and prophecy variables.

The std++ release is mostly a patch release, and contains no major changes. The
full list of changes is documented in the [Iris changelog] and [std++
changelog], respectively.

[Iris changelog]: https://gitlab.mpi-sws.org/iris/iris/blob/master/CHANGELOG.md
[std++ changelog]: https://gitlab.mpi-sws.org/iris/stdpp/blob/master/CHANGELOG.md

Iris 3.2 and std++ 1.2.1 should appear in Coq's opam repository soon. If you
have any questions, don't hesitate to contact us on our [mailing list], or join
the [Iris chat room]. We also welcome bug reports and pull requests at the
[Iris] and [std++] GitLab projects.

[mailing list]: https://lists.mpi-sws.org/listinfo/iris-club
[Iris chat room]: https://mattermost.mpi-sws.org/iris
[Iris]: https://gitlab.mpi-sws.org/iris/iris
[std++]: https://gitlab.mpi-sws.org/iris/stdpp

For examples showing how to use Iris, have a look at the Iris case studies we
maintain in the [examples] repository. We will make sure they are always
compatible with the latest version of Iris. Lecture material for Iris is
available [on our website][lecture]. For further information, visit the [Iris
project page].

[examples]: https://gitlab.mpi-sws.org/iris/examples
[lecture]: https://iris-project.org/tutorial-material.html
[Iris project page]: https://iris-project.org/

These releases of Iris and std++ received contributions from Aleš Bizjak, Amin
Timany, Dan Frumin, Glen Mével, Hai Dang, Hugo Herbelin, Jacques-Henri Jourdan,
Jan Menz, Jan-Oliver Kaiser, Jonas Kastberg Hinrichsen, Joseph Tassarotti,
Mackie Loeffel, Marianna Rapoport, Maxime Dénès, Michael Sammler, Paolo G.
Giarrusso, Paulo Emílio de Vilhena, Pierre-Marie Pédrot, Ralf Jung, Robbert
Krebbers, Rodolphe Lepigre, Simon Spies, and Tej Chajed. Thanks a lot to
everyone involved!

Best,
The Iris and std++ team