[Iris-Club] Iris 3.1, std++ 1.1

[Ralf Jung]

Dear Iris users,

We are happy to announce the release of *Iris 3.1*.  You can find more
information at <http://iris-project.org/>.  This is the Iris release that will
be used at the upcoming Iris tutorial at POPL'18.

For examples showing how to use Iris, have a look at the Iris case studies we
maintain at <https://gitlab.mpi-sws.org/FP/iris-examples>.  We will make sure
they are always compatible with the latest version of Iris.  Lecture material
for Iris is available at <http://iris-project.org/tutorial-material.html>.

This release includes many improvements and extensions, both to the theory of
Iris, its derived constructions, and the Coq infrastructure.  On the Coq side,
we mostly worked on making the interactive proof mode more consistent and more
expressive, accounting for the needs of the growing number of projects that rely
on it.  The full list of changes is documented in our Changelog at
<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/CHANGELOG.md>.

Iris 3.1 should appear in Coq's opam repository soon.  If you have any
questions, don't hesitate to join the recently created Iris chat room at
<https://mattermost.mpi-sws.org/iris>.  We also welcome bug reports and pull
requests at <https://gitlab.mpi-sws.org/FP/iris-coq/>.

Next to Iris 3.1, we are happy to release std++ 1.1: an "extended standard
library" for Coq, which provides many definitions and lemmas for common data
structures such as lists, finite maps, finite sets, and finite multisets, as
well as tactics and other infrastructure for reasoning about these. This library
used to be part of Iris, but has become a separate project since this Iris
release.  More information is available on the project website at
<https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/>.

Both Iris 3.1 and std++ 1.1 are compatible with Coq 8.6.1 and newer.

On behalf of the Iris team,
Ralf