Add mode for Dist

marked this merge request as draft

mentioned in merge request !696 (merged)

added 3 commits

• 9c26f76a...07ab4060 - 2 commits from branch iris:master
• 2b3d5721 - Mode for Dist

Compare with previous version

marked this merge request as ready

added 1 commit

• beebb5e6 - Mode for Dist + CHANGELOG

Compare with previous version

@jung The next step (if/when you want) is to run reverse CI against this branch, right?

Yes, I'll do that now. Thanks for the rebase! FYI, your other branch passed CI on all projects we test without any changes.

Looks like all pipelines passed -- so this does not seem to cause any breakage in our reverse dependencies. Hence I am in favor of landing the change.

Cool. If that's well-automated, after this we can check the same for Equiv; worst-case, we might find more bugs to report upstream.

It's a one-line command to run these tests, so -- sure. ;)

mentioned in merge request !701 (merged)

I have some mixed feelings about this.

One the one hand, due to the Coq bug, this means that some strange unexpected type annotations are needed in client code. One could imagine similar statements from !701 (diffs) involving dist. That said, CI shows we're not doing writing such statements in practice. Also, dist not used that much, aside from writing NonExpansive instances, for defining custom camaras, and for hacking in the model.

So, question here: does the benefit of the Hint Mode outweigh the issues?

I slightly think it does.

"The Coq bug" being https://github.com/coq/coq/issues/14441, I assume? It's always good to add some links for people reading this in the future. ;)

I don't have any feeling for the scope of that bug, so for me the fact that all CI passed is a good enough signal that this is safe.

I don't have a clear feeling for it either (there's also no response from the Coq team yet, so we don't know what's the cause).

I tried to cook up a similar example for dist as we have for equiv in https://github.com/coq/coq/issues/14441 It turns out the version for dist just works. It looks like the interaction between type classes and canonical structures is somehow in our favor here?

From iris.algebra Require Import list.

Global Hint Mode Dist ! : typeclass_instances.

(* succeeds *)
Lemma list_dist_lookup {A : ofe} n (l1 l2 : list A) :
  l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
Abort.

Global Hint Mode Equiv ! : typeclass_instances.

(* succeeds *)
Lemma list_equiv_lookup {A : ofe} (l1 l2 : list A) :
  l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
Abort.

(* fails *)
Lemma list_equiv_lookup `{Equiv A} (l1 l2 : list A) :
  l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
Abort.

So, I think I am in favor of this MR now, provided we add the example list_dist_lookup to the test suite. Then we make sure that if Coq changes, that example remains to work.

added S-waiting-for-author label

added 1 commit

• 5690e7c1 - Add suggested test

Compare with previous version