The Coq mailing list

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

Hi Guillaume,

>>> 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".
> 
> Because I am assuming the library's author is not dumb enough to have a
> hierarchy A/B/C/**/A/B/C.v.
> 
> At some point, we have to accept that we cannot always win against dumb
> or malicious users. They will always find a way to circumvent the system.

Well then why do we even do typechecking, users won't be dumb enough to write
ill-typed code, right? /s

Seriously though, I do not understand this attitude.  No other language that I
know of has a module system as strange as Coq's (maybe this is inherited from
OCaml?), and yet you claim that it's the library author's fault for not taking
care in designing their library to work around this quirk, rather than the
language designer's fault for having designed something strange.  (Probably 
the
language designer had a good reason and this was solving a concrete problem, 
but
putting the blame on the library is just unfair. And you haven't argued for 
why
Coq's semantics make any sense, either.)

This is not about malicious users, it is about people coming to Coq with what 
I
consider reasonable expectations having their code break for reasons that are
really hard to figure because Coq violates assumptions formed when learning
pretty much any other language. Even the notoriously sloppy JavaScript 
requires
precise imports! I still remember my surprise when I learned about "-R"
semantics... it remains a mystery to me how it seemed like a good idea to just
recursively slap everything into the global namespace. And then when "From ...
Require" was introduced I was very surprised to learn about its path matching
semantics, I had not even realized that regular "Require" was not doing
full-path matching either. For what is otherwise a system that is extremely
picky about which terms it accepts (for good reasons!), this stands out like a
sore thumb.

There probably is a reasonable explanation for this. But dismissing the 
concern
as only affecting "dumb" users is not reasonable.

Kind regards,
Ralf