The Coq mailing list

[Théo Zimmermann <theo AT irif.fr>]

Since the module system was mentioned in this thread, and it was
remarked that it is both very powerful and hard to learn because you
basically need to know the background and it is not sufficiently
documented in Coq's own documentation, I'll take the opportunity to
advertise the fact that in 8.12, we have consolidated the
documentation of modules in a single place
https://coq.inria.fr/refman/language/core/modules.html (without
changing much of the content) and it would be a good time for someone
motivated and who appreciates and understands Coq's module system to
propose a partial rewrite of this documentation. As it is mentioned on
this page 
https://github.com/coq/coq/wiki/Refman-improvements-in-8.12-and-beyond,
it needs, at the very least "complete proofreading, more explanations
about Inline, possibly more examples".

Then, back to the original topic, it was noticed that there already
are a couple of issues related to this:
- https://github.com/coq/coq/issues/9839
- https://github.com/coq/coq/issues/11124

So perhaps those can be commented on with additional hindsight,
instead of creating new ones.

Le sam. 19 sept. 2020 à 04:32, Jeremy Dawson
<Jeremy.Dawson AT anu.edu.au> a écrit :
>
>
>
> On 19/9/20 1:01 am, Guillaume Melquiond wrote:
> > Le 18/09/2020 à 16:46, Ralf Jung a écrit :
> >> (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.)
> > The reason is the standard library of Coq. It is important to understand
> > how painful it would be to use if Imports had to be fully qualified.
> > Here is a quiz for you. Which of the following are correct?
> >
> > 1.a Require Coq.List.List.
> > 1.b Require Coq.Lists.List.
>
> If the Coq module system really were based to a significant extent on
> the SML module system, surely the answer would be both are correct, with
> a trivial amount of extra code.  I think the code would look something
> like this
>
> structure Coq = struct
>    structure List = struct
>      <the stuff in List>
>    end ; (* structure List *)
>    structure Lists = List ;
> (* or, if that does more than you want
>    structure Lists = struct
>      structure List = List.List ;
>    end ; (* structure Lists *)
> end ; (* structure Coq *)
>
> One of the problems, as I understood it (accepting that it seems so
> bizarre that I might well be mistaken) is that to compile a Coq source
> file, you have to know where in the logical hierarchy of logical paths
> it is going to be used.  Which is certainly not something I've
> experienced in 25 years using SML (though this, admittedly, would
> potentially vary between SML implementations).
>
> Jeremy
>