The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

I'm grateful to Thomas to raise this important issue on which no
progress has unfortunately been made for a while.

In order to ease the reviewing of extensions or corrections of
existing libraries by users, having guidelines seems indeed a
prerequisite. One of the obvious problem is that Coq standard library
is an heterogenous collection of works made at different times of the
history of Coq when tactics were not necessary very powerful, when the
specification language was not necessarily as developed as it is now
and when some convenient formalization or proving techniques were not
yet "invented".

Nevertheless, I started to make public on Cocorico a set of tentative
guidelines that "we" expect users to follow before submitting an
addition or a modification to a library. I put the text on the wiki
(page http://coq.inria.fr/cocorico/HowToContributeToTheStandardLibrary)
so that anyone can discuss the guidelines, add new questions about
unclear or missing recommendations, comment about whether such or such
guideline is reasonable or not, etc. I hope that at some time, we will
have converged to something comprehensive and useful for everyone.

Now, about "a repository for such extensions, to gather lemmas that
could be useful to other people", I fully support this idea and as far
as I can judge this is connected to the MathWiki project developed at
Nijmegen. This is certainly not an easy project to set up but this is
something I think our community would make a great usage of.

One other direction (but a more static one) is to use the Coq user
contribution repository (http://coq.inria.fr/pylons/contribs/index)
and equip it with seeking and rendering tools such as the ones the
Matita group at Bologna developed (Whelp and Helm). There are ongoing
works on this side but unfortunately not ready yet. In the meantime,
don't hesitate to contribute to the repository though.

Hugo

On Wed, Mar 09, 2011 at 02:15:30PM +0100, Thomas Braibant wrote:
> 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
> 
>