[Iris-Club] Final breaking changes before Iris 3.0

Ralf Jung jung at mpi-sws.org
Fri Dec 9 17:42:48 CET 2016


Hi all,

Over the last few days, a few changes that could affect Iris users have
been merged (and one more is coming).  On the plus side, I think we
should just call what we got then "Iris 3.0" so that there's finally a
canonical version to refer to. :)
The plan is for Iris 3.0 to work with both Coq 8.5 and 8.6.  After that,
we will drop support for Coq 8.5 as soon as possible (i.e., as soon as
there is an ssreflect release that supports Coq 8.6).

I will briefly discuss the changes that happened.

## Atomicity

The definition of atomicity changed to make more things atomic.
Specifically, an expression is now atomic if it reduces in one step to
something that doesn't reduce further.  The lemma val_irreducible should
help you to port your proofs.

## Blocking simplification of language terms

To prevent Coq from simplifying language terms (in the deeply embedded
language) too far, we used to make such terms opaque definitions and
relied on the fact that ssreflect's `rewrite /` can unfold such
definitions.  This is no longer the case in the latest ssreflect
development versions, so we had to find something else.  We are now
using the `locked` mechanism of ssreflect.  If you define your own
language and you want your development to be compatible with Coq 8.6,
you will have to do something similar.  See
<https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/34> for further
details.

## Handling of physical state in WP

WP is now parameterized over a predicate on physical state, instead of
using the construction that reflect the entire physical state as one
exclusive piece of ghost state.  This makes the overall infrastructure
simpler for simple languages (in particular, heap_ctx is gone!).  More
complex languages may still have to use the old construction, which is
provided by program_logic.ownp.  Since we don't use that compatibility
layer ourselves, we would appreciate feedback about inconveniences or
missing features.  (Merge requests are the best form of feedback ;)

## Deprecation of dec_agree
[Not yet merged]

I contrived a new agreement construction that has the property of
preserving discreteness of the OFE it works on.  As a consequence,
algebra.agree is now suitable for cases where we previously pretty much
had to use algebra.dec_agree, and the latter is deprecated.  (It can
still be imported as algebra.deprecated.dec_agre_deprecated.)  To get an
idea how porting from dec_agree to agree works, see
<https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c6a626adbe1bf78b34f4e74204b98007f532892d>
or
<https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/02ec729804203eb53327e74b4c7cf5ce853c6d54>.

Of course, you can quite easily keep using the old dec_agree by making a
copy of it (to be prepared for the time when the deprecated module will
be removed).

Kind regards,
Ralf




More information about the Iris-Club mailing list