The Coq mailing list

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

Hi Guillaume,


On 18.09.20 14:44, Guillaume Melquiond wrote:
> Le 18/09/2020 à 14:18, Gaëtan Gilbert a écrit :
>> We perhaps could add a syntax with leading dot, so in
>>
>>     Require .Foo.Bar Baz.
>>
>> Foo.Bar is fully qualified, Baz isn't.
>>
>> (kind of like internet domain names with trailing dot)
> 
> Another possibility would be to relax some requirements of From-Require.
> Currently, "From A.B.C Require D.E.F" means that not only the path
> should start with A.B.C and finish with D.E.F, but also that there
> should be no overlap between A.B.C and D.E.F. If the second constraint
> was removed, then Require would become non-ambiguous for people who have
> to use messy libraries.

I don't see how accepting even more paths for a given import can possibly
resolve any ambiguities? "From A.B.C Require A.B.C" would then match both
"A.B.C" and "A.B.C.*.A.B.C".

Also I think having unambiguous identifiers is important in general, no matter
how messy the library. If anything I'd argue that the Coq standard library is
messy if it requires such interesting import semantics. After all, to pick a
random example, when I refer to lemma "foo" in Coq it also doesn't just pick 
any
lemma that has "foo" somewhere in its name -- it tests for equality, not a
substring. That would be a rather obscure way of name resolution. The Coq 
import
semantics are just as obscure in my eyes.

But I understand this is very hard to change now. I am still curious how we 
even
got here -- is this import semantics inherited from some other language, or 
did
Coq introduce it?

Kind regards,
Ralf