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

[Dan Frumin]

Dear Ralf,

The "Coq example files" button at the tutorial web page 
<http://iris-project.org/tutorial-material.html> is currently 404'd.

It points to 
https://gitlab.mpi-sws.org/FP/iris-examples/blob/master/theories/iris-lecture-notes/
instead of 
https://gitlab.mpi-sws.org/FP/iris-examples/tree/master/theories/lecture_notes

Best,
Dan

On 19-12-17 19:39, Ralf Jung wrote:
> 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
>