Iris 3.6 and std++ 1.7 released

Announcements
1

We are happy to announce the release of Iris 3.6 and std++ 1.7. Iris is a concurrent separation logic framework for Coq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Coq.

The highlights and most notable changes of Iris 3.6 are:

  • Coq 8.15 is now supported, while Coq 8.13 and Coq 8.14 remain supported.
    Coq 8.12 is no longer supported.
  • Support for discardable fractions (dfrac) has been added to gmap_view
    authoritative elements, and to the mono_nat library. See below for other
    dfrac-related changes.
  • A new mono_list algebra provides monotonically growing lists with an
    exclusive authoritative element and persistent prefix witnesses. See
    iris/algebra/lib/mono_list.v for details. An experimental logic-level
    library wrapping the algebra is available at
    iris_staging/base_logic/mono_list.v; if you use it, please give feedback on
    the tracking issue
    iris/iris#439.

Further details are given in the changelog at CHANGELOG.md · master · Iris / Iris · GitLab

This release was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with
contributions from Dan Frumin, Jonas Kastberg Hinrichsen, Lennard Gäher,
Matthieu Sozeau, Michael Sammler, Paolo G. Giarrusso, Ralf Jung, Robbert
Krebbers, Simon Friis Vindum, Tej Chajed, and Vincent Siles. Thanks a lot to
everyone involved!

For std++, Coq 8.15 is newly supported by this release, and Coq 8.11 to 8.14 remain supported. Coq 8.10 is no longer supported.

This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with contributions from Glen Mével, Jonas Kastberg Hinrichsen, Matthieu Sozeau, Michael Sammler, Ralf Jung, Robbert Krebbers, and Tej Chajed. Thanks a lot to everyone involved!

For further details, see the full changelog at CHANGELOG.md · master · Iris / stdpp · GitLab

Both packages are available in the Coq opam registry. For further information and installation instructions for Iris and std++, see the respective project websites:

2 Likes