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

[Ralf Jung]

Hi Jeehoon,

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

There is no good reason to demand a proof that CMRAs be complete.
`uPred M` is complete for any OFE M.
We would like to use a CMRA that actually is an OFE, but not a COFE;
this change is necessary to make that possible.
(In case you are interested, the merge request
<https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/22> is the one
depending on this change.)

> 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.

Once we have a stable release of the Iris 3 Coq, we can talk about
things like this. ;)  However, I think backwards compatibility in Coq in
generally too hard to achieve, i.e., pretty much every release will have
*some* potentially breaking change.  We should try to keep that to a
minimum.  Unfortunately, we don't have the man-power to maintain both a
master branch with breaking changes and a stable branch that only gets
some non-breaking fixes backported.  My hope is just that the speed at
which breaking changes happen will reduce...

"What is a stable Iris 3 release waiting for", you may ask?  Good
question... certainly all the open merge requests need to be resolved
one way or another.  We are also experimenting with various ideas that
would let us split Robbert's prelude into a separate project that Iris
just depends on.  As far as I am concerned, once we settled those topics
(and updated the documentation to the OFE change), we can call it 3.0 --
but others may have more ideas for things that should go in before 3.0
is tagged.

Kind regards,
Ralf