The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> Le 17/09/2020 à 16:19, Abhishek Anand a écrit :
>> I used to think that using disjoint logical prefixes for different
>> libraries and always using fully qualified names in Require Imports
>> would suffice for avoiding errors due to incorrect files being imported.
>> However, it was recently pointed out to me that this is not sufficient:
>> Suppose we have 2 .vo files, one with fully qualified name A.B.C and
>> another with fully qualified name B.C.
>> Now we suddenly have no reliable way to Import the latter file unless
>> there is a way to tell `Require Import` that the name should be
>> interpreted in a fully qualified manner.
>> Is there a workaround for this?
> 
> You can use:
> 
>   From A Require B.C.
>   From B Require C.
> 
> If you have three files named A.C, A.B.C, and B.A.C, then there is no
> foolproof way to load A.C. But this is the author of library A being
> malicious. Just stop using library A.

I cannot see any malice here, maybe just slightly messy naming.
But Coq should support unambiguous imports no matter how messy or questionable
the naming choices of any library involved are.

I've had quite weird problems in the past caused by stale .vo files being 
picked
up by ambiguous imports, so I'd be all for a way to ensure that all imports 
are
unambiguous. (In fact I am quite surprised that ambiguous imports exist at 
all,
that seems quite contrary to Coq's usual design geared towards precision. No
other language I work or worked with has ambiguous imports the way Coq does --
Python, Java, C++, Rust all do not have this problem.)

Kind regards,
Ralf