The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

The Coq module system dates from V7: 
https://coq.inria.fr/refman/history.html#versions-7
>The version V7 is a new implementation started in September 1999 by 
Jean-Christophe Filliâtre. This is a major revision with respect to the internal 
architecture of the system. The Coq version 7.0 was distributed in March 2001

I don't know when Require was introduced but surely it was earlier than that, 
so its interaction with then nonexistent modules was not considered.

Gaëtan Gilbert

On 18/09/2020 16:54, Andrew Appel wrote:
> Oops, let me clarify.
>
> The sloppiness of Require paths, which is the subject of this thread, has 
> bothered me for years.  That's the +1.
>
> Regarding the Coq module system -- I love the Coq module system, which is 
> based on the OCaml module system, which is based on the Standard ML module 
> system, a landmark achievement in computer science developed primarily by 
> David MacQueen between 1984 and 1995, with contributions from Mads Tofte and 
> Xavier Leroy.
>
> -- Andrew
>
>
> ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
>
>     *From: *"appel" <appel AT princeton.edu>
>     *To: *"coq-club" <coq-club AT inria.fr>
>     *Sent: *Friday, September 18, 2020 10:50:00 AM
>     *Subject: *Re: [Coq-Club] option to disable partially qualified Require 
> Imports
>
>     +1
>
>     
> ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
>
>         *From: *"Ralf Jung" <jung AT mpi-sws.org>
>         *To: *"coq-club" <coq-club AT inria.fr>, "Guillaume Melquiond" 
> <guillaume.melquiond AT inria.fr>
>         *Sent: *Friday, September 18, 2020 10:46:09 AM
>         *Subject: *Re: [Coq-Club] option to disable partially qualified 
> Require Imports
>
>         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