**Hugo Herbelin**
(8418f2fb)
*
at
30 Nov 14:31
*

Adapt to edestruct on variables clearing the variable like destruct...

*
... and
78 more commits
*

What Coq PR #12984 does is that at re-import time, printing rules which were overriden by intermediate declarations are reactivated (which is a more natural behavior than the previous one).

As indicated in a previous report on the stdpp repository, the Coq PR breaks the `heap_lang.v`

test by reimporting `Utf8`

on top of `bi.weakestpre`

, so that the "Texan" notations defined there are overriden by the `∀`

notation defined in `Utf8`

.

The existing reimport of `heap_lang.lang`

in `heap_lang.v`

test does not seem needed anymore. However, reimporting `bi.weakestpre`

helps, what the current Iris MR does.

I don't understand well enough the file organization of iris to be able to tell if this fix is really good. Moreover, it fixes the test file, but I guess that other changes would have to be done to preserve a working environment which prints objects as expected. Reimporting `bi.weakestpre`

might hopefully be enough but I have no idea if this will really be so.

@herbelin are you okay with closing this MR until we figured out where we want to go?

Yes closing (looking like we are going towards the ordering-by-precision solution).

What Coq PR #12984 does is that at re-import time, printing rules which were overriden by intermediate declarations are reactivated (which is a more natural behavior than the previous one).

As indicated in a previous report on the stdpp repository, the Coq PR breaks the `heap_lang.v`

test by reimporting `Utf8`

on top of `bi.weakestpre`

, so that the "Texan" notations defined there are overriden by the `∀`

notation defined in `Utf8`

.

The existing reimport of `heap_lang.lang`

in `heap_lang.v`

test does not seem needed anymore. However, reimporting `bi.weakestpre`

helps, what the current Iris MR does.

I don't understand well enough the file organization of iris to be able to tell if this fix is really good. Moreover, it fixes the test file, but I guess that other changes would have to be done to preserve a working environment which prints objects as expected. Reimporting `bi.weakestpre`

might hopefully be enough but I have no idea if this will really be so.

**Hugo Herbelin**
(84f3f086)
*
at
24 Oct 15:19
*

Compatibility with Coq PR #12984 about new reimport of printing rules.

*
... and
1496 more commits
*

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

Thanks!

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.

**Hugo Herbelin**
(317813ff)
*
at
02 Sep 17:43
*

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.

**Hugo Herbelin**
(a4cf7c56)
*
at
31 Aug 10:44
*

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

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.

**Hugo Herbelin**
(3a6be514)
*
at
31 Aug 09:47
*

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

**Hugo Herbelin**
(5f82722e)
*
at
18 Feb 12:31
*

Adapt to Coq PR #11327 (coercions to funclass inherit implicit argu...

*
... and
821 more commits
*

**Hugo Herbelin**
(5712dba8)
*
at
18 Feb 06:27
*

Adapting to Coq PR #11261: do not print types of variables with imp...

*
... and
819 more commits
*

Ah, if the space was not intended, that's indeed another story. So, please withdraw this PR if !336 (merged) is adopted instead. Best.

The Coq PR is not currently blocked on merging the Iris PR, but, for CI consistency, the Iris PR will have to be merged at the same time the Coq PR is merged.

(Currently and anecdotically, the iris test on the Coq PR is failing due to a username/password failure on fetching my mpi-sws gitlab branch. I don't know if it is important or not.)

The Coq PR is not fully ready yet: it is waiting for some documentation to be added. So, the time when a synchronization shall be needed might be days or weeks.

I suspect this will rather be 8.12 (unless it is argued to be an urgent fix).

Wrt blocking, I'm unsure I exactly understood which PR (Coq or Iris) you are talking about.

PS: I forgot to rebase against your current master. So now did I.

**Hugo Herbelin**
(33272af5)
*
at
12 Nov 18:15
*

Adapting to Coq PR#10832: formats associated to a given interpretation

*
... and
364 more commits
*