Fix `Export` order for `length`. Remove `length` hack in strings.

The notation in strings was a hack to shadow the length function on strings with those on lists.

@msammler and I figured out how to change the imports to fix this problem without the hack. Basically, stdpp.base exports Coq.Strings and Coq.List in the right order, so the shadowing is done right. As a consequence Coq.Strings should never be exported by hand.

This approach seems to work among all supported Coq versions.

We also added a test.

added 1 commit

• 7f59be76 - Remove `length` notation in `strings` file.

Compare with previous version

I have no clue if this is compatible with older Coq versions, so let's see what the CI says.

It appears to break with any Coq version < 8.11.

It's probably related to the 8.11 import changes then. Is there some other alternative for those versions?

I looked again at the problem and found out the following: If you do

From stdpp Require Import strings.
Goal length [1] = 1%nat.

or

From stdpp Require Import prelude.
From stdpp Require Import strings.
Goal length [1] = 1%nat.

length is printed as length (as it should be). However, if you do

From stdpp Require Import strings.
From stdpp Require Import prelude.
Goal length [1] = 1%nat.

length is printed as strings.length. The problem is that stdpp.prelude exports stdpp.base, which exports Coq.List. In this case the pretty printer tries to print the notation (now available as strings.length since length refers to the definition on lists) instead of the definition, which in this case is uglier. The problem is that many files Require Export stdpp.prelude since it is part of iris.algebra.base, thus adding From stdpp Require Import strings. to the beginning of files would not work. One would need to add it after all other imports. One other work around could be to add strings to stdpp.prelude (I have not tried this).

So a possible solution is to put strings at the right place in prelude.

Then in Iris and friends we need to make sure to never import strings?

Doesn't sound great, but it's surely an improvement over the status quo. Do you want to try this?

See !139 (closed) where I tried the change to stdpp and it seems to work. No change to Iris seems to be necessary. Importing strings directly should be fine, there is only a problem if you import stdpp.base after stdpp.strings.

added 29 commits

• 7f59be76...4b0c93cb - 28 commits from branch master
• 7d981af6 - Fix `Export` order for `length`. Remove `length` hack in strings. Add a test.

Compare with previous version

mentioned in merge request !139 (closed)

changed title from {-Remove length notation strings-} to {+Fix Export order for length. Remove length hack in strings.+}

changed the description

The added test only works on Coq versions which have ref testing enabled (i.e. 8.10 and 8.11).

added 1 commit

• f3842eb3 - Use `Check` instead of `About` to hopefully have stable test output among Coq versions.

Compare with previous version

added 2 commits

• 7a12d51e - `length` notation in `base` to also fix `length` in Coq ≤ 8.10.
• e5d93fb3 - More testing.

Compare with previous version

added 2 commits

• dc849367 - `length` notation in `base` to also fix `length` in Coq ≤ 8.10.
• d6370287 - More testing.

Compare with previous version

It seems rather excessive and potentially problematic to export String to every single user of std++. (I am not sure what Datatype contains.)

Datatypes contain all the basic data types like bool, list, unit, and some basic functions on those, like length.

It seems rather excessive and potentially problematic to export String to every single user of std++.

If things are properly shadowed it should not hurt. Note that we already export tons of stuff like Utf8, Setoids, Program stuff, etc.

Anyway, to assess if it causes any problems, could we run the CI on all Iris reverse dependencies?

If things are properly shadowed it should not hurt.

Well this is still a gross misuse of the Coq module system. Just because we in Iris are not very careful about what we import, and rely on "C-style namespacing" to disambiguation, that does not mean we should force this on all Iris users.

could we run the CI on all Iris reverse dependencies?

I can do that. (I can also tell you how to do it so you don't have to wait for me each time, and I don#' have to forward the results each time.^^)

FWIW, given the way we "use" the module system, I do not think that passing CI would indicate that this is not a problem. So at best this can give us a negative signal (it breaks even our own code), but I do not think it can give us a positive signal.

added 1 commit

• 6c604e56 - More testing.

Compare with previous version

The CI run found two failures, lambda-rust master and weak_mem:

• https://gitlab.mpi-sws.org/iris/lambda-rust/-/jobs/64059
• https://gitlab.mpi-sws.org/iris/lambda-rust/-/jobs/64060

My guess what is going wrong with the The term "bool" has type "Set" while it is expected to have type "type". failure in lambda-rust (https://gitlab.mpi-sws.org/iris/lambda-rust/-/jobs/64059#L230): There is a lambda-rust type called bool in lambda rust and there is a Coq Set called bool in Datatypes. This is a violation of the usual c-style namespacing we do and this is why this MR break this code. Note that the failure is in int.v which first imports bool and then (ordering is important) imports programs. https://gitlab.mpi-sws.org/iris/lambda-rust/-/blob/master/theories/typing/int.v#L3 [rograms transitively exports stdpp.base which with this MR exports the Coq bool due to the export of Datatypes. Thus with this MR bool in int.v refers to the Coq bool, while without this MR it refers to the lambda rust bool. Note that my other MR !139 (closed) would probably also run into this problem as it would also make programs export Datatypes.

This is all very messy and I don't know what the best solution is. I see the following options:

• accept this MR (or !139 (closed)) and accept the breakage
• I thought there was a version which works on all Coq versions and does not rely on exporting Datatypes but prints Datatypes.length on Coq versions before 8.11. (Was it making the notation in strings.v parsing only?) This would make the problem for users of 8.11 go away and change strings.length to Datatypes.length for users for older Coq versions.
• do nothing (please not)

accept this MR (or !139 (closed)) and accept the breakage

s/accept/fix/

I'm afraid that's the most pragmatic choice. I would be in favor of this.

I thought there was a version which works on all Coq versions and does not rely on exporting Datatypes but prints Datatypes.length on Coq versions before 8.11. (Was it making the notation in strings.v parsing only?) This would make the problem for users of 8.11 go away and change strings.length to Datatypes.length for users for older Coq versions.

That's removing the Notation length in base.v. I don't think that affects the lambdarust problem.

I'm still opposed to increasing the reexports of stdpp.base. That's a very heavy hammer you are swinging here.

In another thread you wrote:

Well this is still a gross misuse of the Coq module system. Just because we in Iris are not very careful about what we import [..]

I don't think there is a way to use Coq's module system properly, i.e., to not abuse it. As far as I am concerned it's broken beyond repair.

When this issue came up on coq-club, a few people reported that they did use it, and seemed somewhat surprised by our issues with it.

You don't have to Import everything, doing Require most of the time gets you a long way. You can also split a file like

Definition auth := ...

Module auth.
(* Auth lemmas, without `auth_` prefix. *)

We tried this for bi and friends, and it doesn't work too awesome either. Especially if the lemmas are not all in a single file.

I'm still opposed to increasing the reexports of stdpp.base. That's a very heavy hammer you are swinging here.

FWIW: Do you have another proposal, apart from "do nothing (please not)"?

If I understand correctly that this is a problem only for old Coq versions, then honestly I think it is better to leave it unfixed for them than to add this reexport.

We currently support 4 previous Coq versions (until 8.7), so this means we can fix this problem only in two years.

I'm not sure this is worth waiting that long, plenty of people are very confused about the current strings.length.

Now we have !144 (merged), so let's see how well that works.

What I meant is otherwise I think a reasonable solution would fix the problem on Coq 8.11 only, and leave Coq 8.10 broken, without adding the reexport. I am not sure if one of the candidates that @msammler considered satisfies this.

Oh, right, the discussion is a bit defused (since it's in many issues/MRs), so that's yet another alternative. @msammler could you test that !144 (merged) indeed works with Iris and RefinedC?

mentioned in merge request !144 (merged)

There is another option which I tried here and which seems to work without adding new exports: !144 (merged)

merged

Wait @robbertkrebbers why did you merge this? Please revert, this is the one I did not agree to.

Ah I didn't realize @msammler based his MR on this. I think we should have squashed that to avoid noise in the history. Oh well, too late now.^^

Is there a way to flag this MR as "closed" instead of "merged" in Gitlab?

I don't think so. The MR has, in fact, been merged after all -- the commit you were asking to include in the repository, is now included in the repository. That's what a merge is.