The Coq mailing list

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

Hello everyone,

We are pleased to announce the release of Iris 3.3, a concurrent separation
logic framework for Coq. For an overview of the numerous research projects
employing Iris, see <https://iris-project.org/>. Iris 3.3 is accompanied by
std++ 1.4, an extended "standard" library for Coq.

This Iris release does not have any outstanding highlights, but contains a 
large
number of improvements all over the board. For instance:

* heap_lang (the default programming language shipped with Iris) now supports
  deallocation as well as better reasoning about "invariant locations"
  (locations that perpetually satisfy some Coq-level invariant).
* Invariants (inv N P) are more flexible, now also supporting splitting and
  merging of invariants with respect to separating conjunction.
* Performance of the proofmode for BIs (instances of the "Bunched Implication"
  algebra) constructed on top of other BIs (e.g., monPred) was greatly 
improved,
  leading to up to 70% speedup in individual files. As part of this 
refactoring,
  the proofmode can now also be instantiated with entirely "logical" notion of
  BIs that do not have a (non-trivial) metric structure, and still support
  reasoning about ▷.
* The proof mode now provides experimental support for naming pure facts in
  intro patterns.  See <https://gitlab.mpi-sws.org/iris/string-ident> for
  details.
* Iris now provides official ASCII notation. We still recommend using the
  Unicode notation for better consistency and interoperability with other Iris
  libraries, but provide ASCII notation for when Unicode is not an option.
* We removed several coercions, fixing "ambiguous coercion path" warnings and
  solving some readability issues.
* Coq 8.10, 8.11, and 8.12 are newly supported by this release, and Coq 8.7 
and
  8.8 are no longer supported.
Further details are given in the full changelog at
<https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md>.

This release of Iris received contributions by Abel Nieto, Amin Timany, Dan
Frumin, Derek Dreyer, Dmitry Khalanskiy, Gregory Malecha, Jacques-Henri 
Jourdan,
Jonas Kastberg, Jules Jacobs, Matthieu Sozeau, Maxime Dénès, Michael Sammler,
Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Friis Vindum, Simon
Spies, and Tej Chajed.

For std++, Coq 8.12 is newly supported by this release, and Coq 8.7 is no 
longer
supported. For further details, see the changelog at
<https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md>. This 
release
of std++ received contributions by Gregory Malecha, Michael Sammler, Olivier
Laurent, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, sarahzrf, and Tej 
Chajed.

Thanks a lot to everyone involved!

Both packages will be available in the Coq opam registry shortly. 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

Best,
The Iris and std++ teams