Home

Awesome

Contributing Code of Conduct Zulip

coq-community

A project for a collaborative, community-driven effort for the long-term maintenance and advertisement of Coq packages.

Note that this README (the manifesto) is a work in progress and is meant to be collaboratively improved. Please contribute!

Who runs this organization?

This organization is run by volunteer Coq users. Everyone is welcome (you don't need to be a very experienced Coq user to participate). Please get involved!

What are its goals?

Collaborative maintenance of Coq packages and tools

Projects can be hosted in coq-community whenever any of the following is the case:

Each project under the umbrella of coq-community has one or several official maintainer(s), but the maintenance effort is done collaboratively. Users need not be afraid of volunteering to be the official maintainer of a coq-community project because they can step down at anytime. Changing the maintainer of a coq-community project can be done very easily without the hassle of moving its location too.

Maintenance is allowed to go much further than just updating the package to keep it compiling with newer Coq versions. It can also include refactorization of the code, uniformization of the style, merging with other packages, taking pieces out to put them in other libraries, and even removal of some parts that are not raising sufficient interest. These changes must, nonetheless, always be done with consideration for compatibility as soon as the package is a library, plugin or tool that has users.

Collaborative writing of documentation

Some Coq proofs present a particular pedagogical interest because their statements are easy to understand, but they require some non-trivial mathematical tools and their mechanization illustrates interesting proof patterns, or demonstrate the use of specific libraries. They can be used as the basis for tutorials which explain the tricks and interesting parts.

coq-community hosts several such documentation projects. Among them, Hydras & Co. collects libraries of formalized mathematics for inspiration and entertainment, including detailed documentation and exercises. Your contributions are welcome!

Advertising interesting packages

Not all the packages that are transferred to coq-community have the same initial quality. While this should not stop packages from being taken over, and new maintainers should strive to improve the package quality, some editorial work is also required to put forward the most interesting packages, be it for their usefulness as a library or plugin, because they demonstrate interesting proof techniques, or because they represent an important achievement.

Currently, the website highlights a selection of packages with ⭐ and warns about some others with ⚠️ to inform users that some packages are more recommended for reuse than others. Come chat with us if you want to participate in this editorial work.

FAQ

Contributing

Position in the Coq ecosystem

Best practices

Process / organizational aspects

History

Is anything still unclear? Please open an issue or chat on Zulip to ask a question.