Another try at removing strings.length

See discussion in !129 (merged) The idea of this version is to have two notations, one which shadows the bad definition Strings.length and the other which shadows the bad Notation List.length, which is bad because it is parsing only.

mentioned in merge request !129 (merged)

changed the description

Wait, so are you saying that on Coq 8.11, length already behaves correctly now, and the remaining problem that !29 (merged) and this one are fixing only arises on Coq 8.10 and older?

I think with 8.11 length behaves correctly if we remove all hacks. See !129 (7f59be76), but that breaks on 8.10.

I think this is only the case if we add a export of Datatypes to base as !129 (7f59be76) does, which would be a breaking change as discussed in !129 (merged). I updated the comment here (before it was just copy pasted from !129 (merged)).

Another alternative is to patch this issue in Iris. Pretty much all of Iris exports String anyway.

Then, when we drop support for Coq versions prior to 8.11 in a couple of years we can remove all hacks.

I am not sure what that Iris patch would look like, but sure.

Oh wait, you mean fix it by reexporting string there? Well, not great, but better than doing it here.

Or can this also be fixed by avoiding string better in Iris?

Note that if !144 (merged) actually works in Iris, RefinedC, and friends, that would be preferred and my suggestion is void.

Or can this also be fixed by avoiding string better in Iris?

No idea, all of this is black magic... :(

I think fixing it in stdpp is the least brittle solution. I think we could also solve this problem by carefully arranging all exports in Iris, but that seems very brittle.

added 1 commit

• 66664b37 - another try

Compare with previous version

Should I trigger a CI run of iris and its reverse dependencies for this MR?

I triggered the builds.

The run is done, there were no failures.

Could we test that occurrences of length in Iris and RefinedC are indeed printed correctly? If so, then I think we should merge this.

Since I checked pretty printing of some samples in reverse dependencies, I'm going to merge. Thanks all.

mentioned in commit b4103098

merged