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

[Ralf Jung]

Hi Dan,

thanks for pointing this out, it is fixed now.

; Ralf

On 20.12.2017 11:11, Dan Frumin wrote:
> 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
>>
>