Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Initial commit. Draft README and CONTRIBUTING.
- Loading branch information
0 parents
commit 8350bf2
Showing
6 changed files
with
177 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
--- | ||
name: Change of maintainer | ||
about: When a maintainer wants to step down or has become unresponsive. | ||
--- | ||
|
||
## Change of maintainer ## | ||
|
||
**Project name and URL:** | ||
|
||
**Current maintainer:** | ||
|
||
**Status:** | ||
|
||
**New maintainer:** looking for a volunteer <!-- update if you are a volunteer / know a volunteer --> | ||
|
||
If no volunteer are found, the project will be marked as unmaintained until a new one is found. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
--- | ||
name: Meta-issue | ||
about: To ask questions / discuss about the organization / process of coq-community. | ||
--- | ||
|
||
## Meta-issue ## | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
--- | ||
name: Move a project to coq-community | ||
about: When you want to propose a new project for inclusion in coq-community. | ||
--- | ||
|
||
## Move a project to coq-community ## | ||
|
||
**Project name:** | ||
|
||
**Current URL:** | ||
|
||
**Kind:** pure Coq library / OCaml plugin / extractable program / formalization of a mathematical theorem / ... | ||
|
||
**License:** | ||
|
||
**Description:** | ||
|
||
**Status:** | ||
|
||
**Previous maintainer:** | ||
|
||
**New maintainer:** looking for a volunteer <!-- update if you are a volunteer / know a volunteer --> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
*~ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,65 @@ | ||
# Contributing guide # | ||
|
||
This is a shared contributing guide applying to all the projects of | ||
coq-community, including this meta-project. | ||
|
||
*Note this contributing guide itself is a work in progress and is meant to be | ||
collaboratively improved. Please contribute!* | ||
|
||
## Proposing a new package ## | ||
|
||
[Open a new issue using the appropriate template][move_project]. | ||
Fill in the requested information. In particular here are some requirements to | ||
move a project to coq-community: | ||
|
||
- The project must have an open source license (non-commercial / academic | ||
licenses are not acceptable). | ||
- The main authors of the package must either consent to this move or be | ||
completely unresponsive. Therefore, once a project is proposed, we will | ||
open an issue at the original project URL (or send an e-mail when this | ||
option is not available) to try to get consent or at least confirm the | ||
unresponsiveness. Projects that are currently part of | ||
[coq-contribs](https://github.com/coq-contribs) do not require this step. | ||
- We must find a volunteer to become the official maintainer. When | ||
packages are proposed without a volunteer maintainer, the corresponding | ||
issue will be labelled as looking for a maintainer until it finds one. | ||
|
||
## Contributing to a coq-community package ## | ||
|
||
Report bugs on the specific project's issue tracker. Include as many details | ||
as possible (version of the package and how you installed it, version of Coq, | ||
version of OCaml if you built the package yourself...). | ||
|
||
Propose changes by submitting a pull request. This implies that you accept to | ||
put your contribution under the project's license. If the change is a large | ||
one, consider opening an issue first to get an idea whether your change is | ||
likely to be accepted. | ||
|
||
If you are working on a bug fix, report the bug first and self-assign the issue | ||
(you need to be part of the coq-community organization to self-assign an issue, | ||
if you are not you may still post a comment saying you are working on this). | ||
|
||
## Maintaining a coq-community package ## | ||
|
||
As a maintainer, your main role is to handle incoming pull requests (review and | ||
merge them) and to make sure that incoming issues are not left without answer | ||
(even if you don't have to fix them). You may delegate part of this role to | ||
secondary maintainers. | ||
|
||
If you are unresponsive and there are no secondary maintainers, maintainers of | ||
other coq-community projects may act as secondary maintainers. If you are | ||
unresponsive really often or if you wish to step down, you may be replaced by | ||
a new maintainer. | ||
|
||
To replace a maintainer, | ||
[open a new issue using the appropriate template][change_maintainer]. | ||
|
||
## Contributing to this meta-project ## | ||
|
||
The processes and policies of coq-community are very much a work in progress. | ||
Always feel free to [open a meta-issue][meta] or a pull request to propose | ||
some improvements, discuss some policies, etc. | ||
|
||
[move_project]: https://github.com/coq-community/manifesto/issues/new?template=move_project.md | ||
[change_maintainer]: https://github.com/coq-community/manifesto/issues/new?template=change_maintainer.md | ||
[meta]: https://github.com/coq-community/manifesto/issues/new?template=meta.md |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,66 @@ | ||
# coq-community # | ||
|
||
A project for a collaborative, community-driven effort for the long-term | ||
maintenance and advertisement of Coq packages. | ||
|
||
*Note 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. | ||
Please [get involved](CONTRIBUTING.md)! | ||
|
||
## What are its goals? ## | ||
|
||
### Providing a place to maintain packages that were left over by their author ### | ||
|
||
*This is the main objective in the first phase of the coq-community effort.* | ||
|
||
Abandoned packages that are raising enough interest (either because they are | ||
libraries or plugins with many users, or because they represent interesting | ||
mathematical proofs or nice achievements) can be taken over by coq-community. | ||
|
||
Each project under the umbrella of coq-community has an official maintainer | ||
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. That's why it can also make sense for a project which is actively | ||
maintained but not actively developed to move to coq-community. | ||
|
||
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 | ||
or plugin that has users. | ||
|
||
### Collaborative writing of documentation ### | ||
|
||
*This objective will be addressed as part of a second phase of the coq-community effort.* | ||
|
||
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 could be used as | ||
the basis for tutorials which explain the tricks and interesting parts. | ||
Gathering such packages and their documentation could give rise to a new, | ||
interactive “book” that would target advanced Coq learners. | ||
|
||
### Advertising interesting packages ### | ||
|
||
*This objective will be addressed as part of a third phase of the coq-community effort.* | ||
|
||
Not all the packages that will be taken over will be of 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 | ||
will be 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. | ||
|
||
This work will be done by an editorial board which will be constitued of | ||
experimented users and prominent members of the Coq community. They will have | ||
to decide what packages to put forward and on what criteria to take these | ||
decisions. |