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

[Jeehoon Kang]

Dear Ralf,

Could you please briefly explain the motivation behind the change,
especially the preference of OFE over COFE?

Also I would like to ask if you have a versioning scheme for the
development, e.g., breaking changes should increase the major version
number, etc.

Thank you,
Jeehoon

2016-11-23 22:38 GMT+09:00 Ralf Jung <jung at mpi-sws.org>:

> 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
>
> --
> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
> Management: https://lists.mpi-sws.org/listinfo/iris-club
> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org
>



-- 
Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
Software Foundations Laboratory <http://sf.snu.ac.kr>
Seoul National University <http://www.snu.ac.kr>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20161123/6dd3d6d2/attachment.html>