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.