The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

I would love to see improvements/extensions to Coq's standard library.
 As a whole, it seems to be in rough shape.

As a prerequisite for such improvement, it seems critical to develop
an official, written, agreed-upon style guide that is as thorough and
detailed as possible (*).  The library code should (obviously) follow
the style guide and be a perfect model for how users should write
their own code.  Furthermore, whenever a choice is made by a library
contributor that is not covered by the style guide (perhaps because it
is specific to the mathematics of the library), it should really be
accompanied by a clearly explained design rationale.  In general,
anything in a library that is not obvious should be accompanied by
comments.  Adhering to these concepts would help ensure that we end up
with new libraries that are better than what we have now.

(*) The style guide should cover the parts of the Coq code that can be
seen when looking through a library's coqdocs, i.e., the Gallina and
generic tactic definitions.  A style guide for proof scripts would be
a whole other can of worms and seems much less urgent.

 - Aaron

2011/3/9 Thomas Braibant 
<thomas.braibant AT inrialpes.fr>:
> Hi lists,
>
> I wish to brought up to the general attention a point that has been
> discussed on the irc #coq, and later, privately by some of us.
>
> We started a discussion about the state of the standard library, and
> how to contribute to it. Our discussion mainly restated what appears
> on these pages [1,2] , and we can summarize its topic as follows:
>
> "While many users propose to complete and extend some libraries, this
> would require availability from the development team to evaluate and
> review this additions."
>
> We think that the community could profit from a repository for such
> extensions, to gather lemmas that could be useful to other people.
> This raw materials could then be peer-reviewed, improved, and when
> meeting some quality-levels, moved to a blessed repo of more stable
> extensions.
>
> From these lemmas, the community could then organize more coherent
> libraries, but from our point of view, an easy-to-contribute library
> is much better, and we should aim to a state where every ten lines can
> be submitted. At this point it must be stressed that we do not want to
> target whole contribs, only the lemmas that exists "in the
> wild".
>
> Moreover, deciding how to interface a library is a difficult problem,
> and the community could benefit from the co-existence of different
> interfaces for the same theories: it would allow to assess which kind
> of interface is best suited for each kind of work.
>
> While the starting point is that contributing to the standard library
> involve some work from the developers, and that we should lift this
> burden, there must be a middle ground between "every patch reviewed by
> the Coq-devs" and "not involving them at all". Such a middle ground
> could be, e.g., to discuss and settle a naming policy, whose
> implementation would be handled by the community. Or to state a list
> of problems that requires attention.
>
> Of course, this exercise would only be sensible if there was a
> willingness from users to base their code on it, so some kind of
> stability from the blessed part is definitely required; another
> motivation would be to consider the folding of some of our changes
> back into trunk, so we should remain compatible with the standard
> lib.
>
> While we also discussed more technical issues like the licensing
> policy (Coq's one?), how to implement the work-flow we described (in
> particular the peer-reviewing), how to avoid ending up in a fork with
> the standard lib (starting with a copy of the std lib, or an empty
> repo), and where to host this library of lemmas (github seems the
> clear winner here), we should defer these questions, till we know of
> the public response to this proposal.
>
> [1] http://coq.inria.fr/cocorico/ReflectionOnStandardLibrary
> [2] http://coq.inria.fr/cocorico/StandardLibrary
>
>
>