The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

Hugo Herbelin wrote:
> 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 think that this is exactly the kind of guidelines that we require.
Moreover, I think it is crucial to evolve a set of guidelines that
apply both for submissions for the std-lib (by themselves), and for
submissions to the ext-lib (since they may end up being added to the
std-lib later). Yet, I do not think this requirement will be too
tough.


> 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.

I think that the MathWiki project is more oriented toward "how user
can contribute". While this is nice by itself, I do not think we want
to go that way: people that want to contribute to something like a
coq-ext-lib will certainly not be afraid of making [svn/git/... up]
before editing the proofs and the files on their own computers. Thus,
I do not see what kind of infrastructure is required otherwise than
some repo, some guidelines (esp. to track the contributions), and some
place for discussions (e.g. a wiki). Maybe some kind of build
automation could be used to ensure that tagged releases compile well,
but I do not think this is mandatory.

> 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.

I did not know of Whelp and Helm (but at the moment
http://helm.cs.unibo.it/browse/ seems broken). Again, this would be
very nice. But it seems that there is some amount of work to be done,
which would be more complicated than a setting up a repo, and
equipping it with coq-doc generation automation. From my point of
view, even if it is easy to be lost in coq-doc generated pages, this
is good enough as a starting point.

To rephrase what I said: I think that starting with too much
requirements in terms of infrastructure/tools would delay the project,
and that we could/should do with a low-cost approach (as long as it
fits, but some people may disagree). I mean, open-source programming
projects do not require big infrastructure to be developed (no
wiki-like interface, no fancy search tools), and yet, they are being
worked on.

Since proofs are programs (pun-intended), we may be able to use the
same tools than the one that are used by software developers.

With best regards,
Thomas