The Coq mailing list

[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