[Iris-Club] Breaking changes in Iris & deprecated symbols / notation

[Ralf Jung]

Hi all,

Over the course of this week, we pushed a couple of breaking changes to
the master branch (with potentially more to come).  In particular, we
changed the algebraic hierarchy to center around OFEs instead of COFEs;
the proof of an OFE being closed is now carried as a separate typeclass.
 CMRAs are just OFEs, they don't have to be proven complete.  If you
defined your own COFEs or CMRAs, you will have to adapt your
definitions.  If you are just using existing COFEs and CMRAs, things
should keep working unchanged -- with one exception: cofeT is now called
ofeT.

To ease porting, we provide a module algebra.deprecated providing
notations for backwards compatibility -- currently, it defines cofeT as
an alias for ofeT, so if you "From iris.algebra Export deprecated"
somewhere in a base file of your development, you can keep using cofeT.

Furthermore, we deprecated the notation ■ for embedding Coq assertions
into Iris.  This notation was both annoying to use (because you had to
write parentheses) and didn't make too much sense (the similarity with □
is asking for trouble).  So instead, we now use ⌜ ... ⌝, which doesn't
need any additional parentheses.  We also got rid of = and ⊥ in the Iris
scope; that was a rather arbitrary selection of Coq connectives to
provide.  Use ⌜x = y⌝ and ⌜x ⊥ y⌝ instead.

The old notations are provided by algebra.deprecated, so you can import
that into your development to ease porting.

The general plan is to provide such deprecated symbols whenever that is
possible without affecting the "main" (non-deprecated) part of Iris.  If
you find something that should be provided a as deprecated symbol,
please let us know -- preferably via a merge request :)

Happy hacking!
; Ralf