The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hello everyone,

we are happy to announce the release of Iris 3.4 and std++ 1.5. Iris is a 
concurrent separation logic framework for Coq; for an overview of the numerous 
research projects employing Iris, see <https://iris-project.org/>. Iris has a 
logo now, so even if you checked out this website before, it's worth another 
look. :)
std++ is an extended "standard" library for Coq.

The highlights and most notable changes of Iris 3.4 are as follows:
* Coq 8.13 is now supported; the old Coq 8.9 and Coq 8.10 are not supported any 
more.
* The new `view` RA construction generalizes `auth` to user-defined abstraction 
relations. (thanks to Gregory Malecha for the inspiration)
* The new `dfrac` RA extends `frac` (fractions `0 < q ≤ 1`) with support for 
"discarding" some part of the fraction in exchange for a persistent witness that 
discarding has happened. This can be used to easily generalize fractional 
permissions with support for persistently owning "any part" of the resource. (by 
Simon Friis Vindum)
* The new `gmap_view` RA provides convenient lemmas for ghost ownership of 
heap-like structures with an "authoritative" view. Thanks to `dfrac`, it 
supports both exclusive (mutable) and persistent (immutable) ownership of 
individual map elements.
* With this release we are beginning to provide logic-level abstractions for 
ghost state, which have the advantage that the user does not have to directly 
interact with RAs to use them.
  - `ghost_var` provides a logic-level abstraction of ghost variables: a 
mutable "variable" with fractional ownership.
  - `mono_nat` provides a "monotone counter" with a persistent witnesses 
representing a lower bound of the current counter value. (by Tej Chajed)
  - `gset_bij` provides a monotonically growing partial bijection; this is 
useful in particular when building binary logical relations for languages with a 
heap.
* HeapLang provides a persistent read-only points-to assertion `l ↦□ v`. (by 
Simon Friis Vindum)
* We split Iris into multiple opam packages: `coq-iris` no longer contains 
HeapLang, which is now in a separate package `coq-iris-heap-lang`. The two 
packages `coq-iris-deprecated` (for old modules that we eventually plan to 
remove entirely) and `coq-iris-staging` (for new modules that are not yet ready 
for prime time) exist only as development versions, so they are not part of this 
release.
* The proofmode now does a better job at picking reasonable names when moving 
variables into the Coq context without a name being explicitly given by the 
user. However, the exact variable names remain unspecified. (by Tej Chajed)

Further details are given in the changelog at 
<https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md>.

This release of Iris was managed by Ralf Jung and Robbert Krebbers, with 
contributions by Arthur Azevedo de Amorim, Dan Frumin, Enrico Tassi, Hai Dang, 
Michael Sammler, Paolo G. Giarrusso, Rodolphe Lepigre, Simon Friis Vindum, Tej 
Chajed, and Yusuke Matsushita.  Thanks a lot to everyone involved!

For std++, Coq 8.13 is newly supported by this release, Coq 8.8 and 8.9 are no 
longer supported.
This release of std++ was managed by Ralf Jung and Robbert Krebbers, with 
contributions by Alix Trieu, Dan Frumin, Hugo Herbelin, Paulo Emílio de Vilhena, 
Simon Friis Vindum, and Tej Chajed.  Thanks a lot to everyone involved!
For further details, see the full changelog at 
<https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md>.

Both packages are available in the Coq opam registry. For further information 
and installation instructions for Iris and std++, see the respective project 
websites:
* https://gitlab.mpi-sws.org/iris/iris
* https://gitlab.mpi-sws.org/iris/stdpp

If you have any questions, feel free to reply to this email, or join our 
community chat room <https://iris-project.org/chat.html>.

Best,
The Iris and std++ teams