The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 18/09/2020 à 15:28, Ralf Jung a écrit :

>> 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.

I don't even understand why we are wasting so much on this issue when it
is still possible to write the following in Coq:

  Cd "/tmp".
  Extraction passwd.

Best regards,

Guillaume