-
Notifications
You must be signed in to change notification settings - Fork 47
Home
Welcome to the coq-ext-lib wiki!
Easy to commit to. Central repository (avoid having several different, and incompatible, yet related contributions).
- We could start with data-structure libraries. A decent replacement to List, ListTheory inspired by what is done in ssreflect seq.
- However, providing a duplicate of the whole standard library is most certainly a bad idea. We could focus on data-structures (and algorithms) that are often handy in programing languages research. (Non exhaustive list include: lists, heterogeneous lists, maps, sets...)
- The whole standard library
Quoting Aaron Bohannon, from Coq-club:
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.
Following in that thread, Thomas Braibant said:
While I agree that such a style guide is crucial, I think that, at the moment, no one can tell whether, e.g., a partial function should return an option, or a default value. Moreover, writing the guide lines on how to write perfect code can take an infinite amount of time.
Later in that thread, Hugo Herbelin answered:
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.