The Coq mailing list

[Gregory Malecha <gregory AT bedrocksystems.com>]

I'd like to add my voice to Ralf's "vote" above. I think that fuzzy matching is an artifact of the somewhat ad-hoc naming in the standard library, e.g. Coq.Lists.List, etc, and it is something that should ultimately go away sooner rather than later in my opinion. In addition to the benefits listed above, you could probably do a lot more with build tooling with exact matching, and that would likely address some (if not all) of the topics that Abhishek has brought up in the past.

On Thu, Sep 17, 2020 at 11:41 AM Ralf Jung <jung AT mpi-sws.org> wrote:

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

--

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING