coqdep spuriously warns about multiple files with the same name

[whonore]

Description of the problem

Given a B.v with From dir.a Require Import A., and the directory structure:

dir/
    a/
        A.v
    b/
        A.v
    B.v

Running coqdep -R . dir B.v prints:

B.vo B.glob B.v.beautified B.required_vo: B.v a/A.vo
B.vio: B.v a/A.vio
*** Warning: in file B.v, 
    required library A matches several files in path
    (found A.v in a and b; used the latter)

So it seems to choose the correct A.v despite the warning. The warning goes away if the line is changed to Require Import dir.a.A. or if -Q is used instead of -R.

Coq Version

master and at least back to 8.10.

[ejgallego]

Indeed this is a bug; we hope to address that once we do the loadpath cleanup after the Dune switch.

On the other hand -R the current semantics of -R seems like a bit dangerous sometimes so it is possible we modify it.

[maximedenes]

I'd need this fixed for stdlib2. @ppedrot it seems that the logic in 31c7542 w.r.t. to this warning is strange: you warn before searching with the From clause. Would you mind having a look?

[ppedrot]

Indeed, the logic looks wrong. I don't remember this code very well though, I wouldn't mind somebody else writing the fix though :/

[Blaisorblade]

FWIW I get the same warnings while using -Q — it might be because I write From A Require Import B to import A.foo.B.
But the Import is still perfectly well-defined...

[Blaisorblade]

As explained in #12251 but not here,

Moreover, coqdep claims that it's choosing the incorrect version of [dependencies, but in fact is choosing the correct version].