<div dir="ltr"><div><div><div><div>Dear Ralf,<br><br></div>Could you please briefly explain the motivation behind the change, especially the preference of OFE over COFE?<br><br></div>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.<br><br></div>Thank you,<br></div>Jeehoon<br></div><div class="gmail_extra"><br><div class="gmail_quote">2016-11-23 22:38 GMT+09:00 Ralf Jung <span dir="ltr"><<a href="mailto:jung@mpi-sws.org" target="_blank">jung@mpi-sws.org</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi all,<br>
<br>
Over the course of this week, we pushed a couple of breaking changes to<br>
the master branch (with potentially more to come).  In particular, we<br>
changed the algebraic hierarchy to center around OFEs instead of COFEs;<br>
the proof of an OFE being closed is now carried as a separate typeclass.<br>
 CMRAs are just OFEs, they don't have to be proven complete.  If you<br>
defined your own COFEs or CMRAs, you will have to adapt your<br>
definitions.  If you are just using existing COFEs and CMRAs, things<br>
should keep working unchanged -- with one exception: cofeT is now called<br>
ofeT.<br>
<br>
To ease porting, we provide a module algebra.deprecated providing<br>
notations for backwards compatibility -- currently, it defines cofeT as<br>
an alias for ofeT, so if you "From iris.algebra Export deprecated"<br>
somewhere in a base file of your development, you can keep using cofeT.<br>
<br>
Furthermore, we deprecated the notation ■ for embedding Coq assertions<br>
into Iris.  This notation was both annoying to use (because you had to<br>
write parentheses) and didn't make too much sense (the similarity with □<br>
is asking for trouble).  So instead, we now use ⌜ ... ⌝, which doesn't<br>
need any additional parentheses.  We also got rid of = and ⊥ in the Iris<br>
scope; that was a rather arbitrary selection of Coq connectives to<br>
provide.  Use ⌜x = y⌝ and ⌜x ⊥ y⌝ instead.<br>
<br>
The old notations are provided by algebra.deprecated, so you can import<br>
that into your development to ease porting.<br>
<br>
The general plan is to provide such deprecated symbols whenever that is<br>
possible without affecting the "main" (non-deprecated) part of Iris.  If<br>
you find something that should be provided a as deprecated symbol,<br>
please let us know -- preferably via a merge request :)<br>
<br>
Happy hacking!<br>
<span class="HOEnZb"><font color="#888888">; Ralf<br>
<br>
--<br>
<a href="mailto:iris-club@lists.mpi-sws.org">iris-club@lists.mpi-sws.org</a> - Mailing List for the Iris Logic<br>
Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" rel="noreferrer" target="_blank">https://lists.mpi-sws.org/<wbr>listinfo/iris-club</a><br>
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org">iris-club-unsubscribe@lists.<wbr>mpi-sws.org</a><br>
</font></span></blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></div></div>
</div>