Swap import of Peano and Utf8 to ensure that Utf8 notations are preferred.

Coq PR #12950, among others changes, gives to import the effect of reactivating the imported notations.

This has an impact for stdpp, e.g. on printing le n m as either m <= n or m ≤ n, due to the order of imports between Utf8.v and Peano.v in base.v.

The Coq PR is still at the beginning of a process of discussion but the change to stdpp is backward compatible (as far as I can judge) and it should be safe to merge it anyway.

Thanks for the MR Hugo. This looks good to me.

@jung, @msammler (since you solved a previous import bug), any opinion?

approved this merge request

Seems reasonable to me, but there should be a comment saying that Utf8 is deliberately last. Maybe it would make sense to separate it into its own statement?

added 1 commit

• a4cf7c56 - Swap import of Peano and Utf8 to ensure that Utf8 notations are preferred.

Compare with previous version

I now added a comment but I don't know all your conventions. So feel free of course to change it as you'd like it to be.

resolved all threads

added 1 commit

• 317813ff - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

The comment is good. Let's merge this. Thanks!

merged

mentioned in commit 897b954e

Thanks for the merge!

Apparently, Coq CI needs an update also of the stdpp version in the opam file of the iris repository so that Coq CI takes into account the change when testing lambda-rust. What is the policy for that? Do I have to submit a PR for the opam file of iris or is there some other protocol? Thanks in advance.

Hi, I still have a problem, now in the Iris heap_lang.v printing test.

With the change of import policy, importing lang from heap_lang reimports Utf8 on top of weakestpre, so that the "Texan" notations defined there are overriden by the ∀ notation defined in Utf8.

For instance, the last test is printed:

  ∀ Φ : val → iPropI Σ,
    True
    -∗ ▷ (∀ (x y : val) (z : Z), True -∗ Φ (x, y, #z)%V)
       -∗ WP let: "val1" := fun1 #() in
             let: "val2" := fun2 "val1" in
             let: "val3" := fun3 "val2" in
             if: "val1" = "val2" then "val" else "val3" 
          {{ v, Φ v }}

instead of

  {{{ True }}}
    let: "val1" := fun1 #() in
    let: "val2" := fun2 "val1" in
    let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
  {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}

Naively reimporting weakestpre after lang to override Utf8 breaks other things, so, I'm unsure about what would be the "right" way to do?

Do you have an idea of what to do? Somehow, it is a bit unexpected that simply reimporting Utf8 breaks a notation such as (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }}) which is clearly more precise than the one provided in Utf8. (Maybe will I try independently to order the notations by precision of the pattern, this will probably be useful anyway.)

@herbelin lang exports the Iris files after std++ and thus Utf8 though, so why would the other notation take precedence to begin with?

Also, this is the std++ repository; it would probably be better if you could open an issue in the Iris repository unless this is likely to be fixable on the std++ side.

mentioned in merge request iris!553 (closed)

resolved all threads