`Require Import Coq.Lists.Streams.` broken between 8.20.1 and 9.0.0

[gregorynisbet-google]

Hello,

I noticed a small compatibility break between 8.20.1 and 9.0.0 regarding the Coq to Rocq rename and the import logic for some things in the standard library, for example Coq.Lists.Streams.

Here is test.sh.

#!/bin/sh

coqc --version

cat <<'EOF' > /tmp/foo.v
Require Import Coq.Lists.Streams.
EOF

coqc /tmp/foo.v

Here is the output for Coq 8.20

$ bash /tmp/test.sh 
The Coq Proof Assistant, version 8.20.1
compiled with OCaml 4.14.2

And here is the output for Coq 9.0.0 . I build it using a different version of OCaml, but that's just because it's the easiest way to get different opam switches and install different versions of Rocq side by side. If I need to (or it is preferable to) build different versions of Rocq with the same version of the OCaml compiler please let me know.

bash /tmp/test.sh 
The Rocq Prover, version 9.0.0
compiled with OCaml 5.2.1
File "/tmp/foo.v", line 1, characters 0-33:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "/tmp/foo.v", line 1, characters 15-32:
Error: Cannot find a physical path bound to logical path
Stdlib.Lists.Streams.

So, we got a deprecation warning but it looks like we failed to fall back to the old name.

[andres-erbsen]

Introduced overtly in e0c2a5f

A quick workaround may be to use From Coq Require Import Streams

@proux01 @SkySkimmer what's the way to provide a proper deprecation trajectory for moved files after rocq-prover/rocq#20601 ? I don't see an obvious way, and given that compat was not provided for this change, I am guessing I'm not the only one. Specifically, the bind seems to be that for fully qualified Require, we'd want a compat file at the old path that re-exports the new path, but adding one would make From-Require for the same module fail due to the linked PR.

I do intend to keep tidying up stdlib, including moving files, so I am quite invested in figuring out a solution.

[gregorynisbet-google]

Coq.Bool.Sumbool is also affected.

Somewhat unrelated, but does Rocq have a way to conditionally run different code depending on the version? I'm trying to keep the project I'm working on compatible between the 8.20.x branch and 9.x branch.

[JasonGross]

Somewhat unrelated, but does Rocq have a way to conditionally run different code depending on the version? I'm trying to keep the project I'm working on compatible between the 8.20.x branch and 9.x branch.

Unfortunately no. See rocq-prover/rocq#15109, rocq-prover/rocq#16351, rocq-prover/rocq#17088, rocq-prover/rocq#13757

[SkySkimmer]

@proux01 @SkySkimmer what's the way to provide a proper deprecation trajectory for moved files after rocq-prover/rocq#20601 ?

That PR doesn't really change the situation does it? Before it we already would have rejected From Stdlib Require Streams. when Stdlib.Streams.Streams and Stdlib.Lists.Streams both exist in the same Stdlib install AFAIK.

[proux01]

use From Coq Require Import Streams

Yes, that's the way it should be done. (or From Coq Require Import Streams. if you need compatibility with < 9.0)
Except a few problematic (duplicated) files (listed in README), it's better to not overqualify imports.

I build it using a different version of OCaml, but that's just because it's the easiest way to get different opam switches and install different versions of Rocq side by side. If I need to (or it is preferable to) build different versions of Rocq with the same version of the OCaml compiler please let me know.

I'm not sure what you mean but you should definitely not have different versions of Coq in path, or install one in same path without having properly cleaned-up the previous one. That's asking for a lot of troubles. You can use opam switches, nix or whatever if you need to experience with different versions.

[andres-erbsen]

It's possible I linked the wrong PR. What I meant is that previously it was okay to have two files with the same name, and now it is not.

Yes, that's the way it should be done ... it's better to not overqualify imports

Really? This is not how any project that I've worked on writes Require statements (other than your contributions). And it seems just brittle for breaking the build on duplicate files. Fully qualified paths are good because they are explicit, and we should have a way to provide compatibility for them.

[proux01]

For historical reasons (at a time From didn't exist), "overqualifying" requirements was the only solution to fix or even prevent conflicts with unrelated libraries. Now, the use of From makes this much easier: one just has to ensure the absence of conflicts inside a single repository / well mastered set of repositories.
The use of the From Lib Require File. form then makes it much easier to rearrange the internals of library Lib, without even having to bother the user, and without any risk.

Arguably, "overqualification" retains a few small advantages:

• when filenames are too short / not very meaningful, it can further document the requirement / prevent typing mistales
• it remains common in some old libraries for historical reasons

[proux01]

Anyway, the original issue is fixed. Discussion on the new topic can continue in rocq-prover/rocq#20792