The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le mercredi 09 mars 2011 à 14:15 +0100, Thomas Braibant a écrit :

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

There exist some other initiatives of this kind for other languages and
it might be worth looking at them. I will only talk about my own
experience with the Boost project [1]. Boost is a C++ repository that
was created to account for all the features that did not make it into
the original ISO/C++ standard library (named STL in the following). It
is also released a bit more often than the STL so that it helps bring
fresh blood to the language. (Think one release every 25 years for the
STL. That's not a typo, it's really a quarter century.) And finally, and
perhaps the most important point for some people, it ensures that the
libraries that are ultimately added to the STL have actually been widely
tested: a library that would have not gone through Boost would have few
chances of being standardized in the STL.

More to the point, Boost is a repository of C++ library. Anybody is free
to submit a new library. Informal (heated) discussions follow. A review
manager is then nominated and checks whether there are enough interest
and whether the library is finished enough. The review wizard sets a
review period: one or two weeks of review, depending on the size of the
library. Note that no two reviews are scheduled the same week, so that
the attention is not diluted. The formal review is public, it happens on
the main mailing-list, and anybody is free to contribute a review. At
the end of the review period, the review manager takes into account all
the reviews (possibly tens of detailed reviews) and summarize them into
an official one, stating whether the library is accepted after minor
revisions, or major revisions (another review is then scheduled), or
rejected.

It looks like a rather heavyweight process, and it is. Much more than an
article submission, since you might have to discuss with tens of
reviewers for several months on an everyday basis. (In the case of my
library, the whole process took about 5 months.) But at the end of the
day, the Boost libraries are "perfect". Meaning that they could be/are
inserted into the STL without raising an eyebrow, and that their
documentation could be/are published into peer-reviewed international
journals.

So Boost isn't what you had in mind, since it is aimed at whole
contributions rather than small additions [2]. But I think it is worth
keeping such a model in mind, since it is rather successful (one million
downloads per month, not counting alternate packaging like deb/rpm/...,
and repository accesses) and it has a major impact on the language: it
is one of the main reasons the language is still widely used.

My point is that the "easy-to-contribute library" might not be the best
choice on the long run. I would be interested in examples of cases where
it was successful.

Best regards,

Guillaume

[1] http://www.boost.org/
[2] Note that Boost has nonetheless an "easy-to-contribute" way: just
submit a bug-report/patch about an existing library and its author will
consider it.