[Iris-Club] Iris 3.0.0

[Ralf Jung]

Hi all,

I just tagged Iris 3.0.0!  This will be the version officially
accompanying the Iris 3.0 paper at ESOP '17 (which is still being
finished).  You can find the sources in the git repository [1].

[1] <https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.0.0>

Here's the full changelog of things that are either changing the theory,
or breaking existing Coq developments for other reasons.  Of course,
many more minor changes have been made everywhere in the development to
try and make things work better.  You can consult the git history for a
full changelog.

> * There now is a deprecation process.  The modules `*.deprecated` contain
>   deprecated notations and definitions that are provided for backwards
>   compatibility and will be removed in a future version of Iris.
> * View shifts are radically simplified to just internalize frame-preserving
>   updates.  Weakestpre is defined inside the logic, and invariants and view
>   shifts with masks are also coded up inside Iris.  Adequacy of weakestpre is
>   proven in the logic. The old ownership of the entire physical state is
>   replaced by a user-selected predicate over physical state that is maintained
>   by weakestpre.
> * Use OFEs instead of COFEs everywhere.  COFEs are only used for solving the
>   recursive domain equation.  As a consequence, CMRAs no longer need a proof of
>   completeness.  (The old `cofeT` is provided by `algebra.deprecated`.)
> * Implement a new agreement construction.  Unlike the old one, this one
>   preserves discreteness.  dec_agree is thus no longer needed and has been moved
>   to algebra.deprecated.
> * Renaming and moving things around: uPred and the rest of the base logic are in
>   `base_logic`, while `program_logic` is for everything involving the general
>   Iris notion of a language.
> * Renaming in prelude.list: Rename `prefix_of` -> `prefix` and `suffix_of` ->
>   `suffix` in lemma names, but keep notation ``l1 `prefix_of` l2`` and ``l1
>   `suffix_of` l2``.  `` l1 `sublist` l2`` becomes ``l1 `sublist_of` l2``. Rename
>   `contains` -> `submseteq` and change `` l1 `contains` l2`` to ``l1 ⊆+ l2``.
> * Slightly weaker notion of atomicity: an expression is atomic if it reduces in
>   one step to something that does not reduce further.
> * Changed notation for embedding Coq assertions into Iris.  The new notation is
>   ⌜φ⌝.  Also removed `=` and `⊥` from the Iris scope.  (The old notations are
>   provided in `base_logic.deprecated`.)
> * Up-closure of namespaces is now a notation (↑) instead of a coercion.
> * With invariants and the physical state being handled in the logic, there is no
>   longer any reason to demand the CMRA unit to be discrete.
> * The language can now fork off multiple threads at once.
> * Local Updates (for the authoritative monoid) are now a 4-way relation with
>   syntax-directed lemmas proving them.

The only incompatibility that has not yet been announced on this mailing
list is the renaming in prelude.list.

Thanks a lot to everyone who was involved in making this release
possible!  We've had contributions by:

* Aleš Bizjak
* Amin Timany
* Dan Frumin
* Derek Dreyer
* Jacques-Henri Jourdan
* Jan-Oliver Kaiser
* Jeehoon Kang
* Joseph Tassarotti
* Ralf Jung
* Robbert Krebbers
* Zhen Zhang

The release is called "3.0.0" because there's now a branch iris-3.0 that
may receive (backwards-compatible) fixes if something critical pops up
that we want to backport.  However, further development is going to
happen only in the master branch.
  The 3.0 branch is also the last series of Iris that supports Coq 8.5;
master is going to depend on Coq 8.6 very soon.

As usual, if you have any questions, comments or other feedback, don't
hesitate to consult this list, the issue tracker [2], or email me directly.

[2] <https://gitlab.mpi-sws.org/FP/iris-coq/issues>

Happy proving!
; Ralf