diff options
Diffstat (limited to 'CONTRIBUTING.md')
| -rw-r--r-- | CONTRIBUTING.md | 75 |
1 files changed, 58 insertions, 17 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index a0139e422d..d9adaf5dc7 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -17,8 +17,8 @@ well. - [Writing tutorials and blog posts](#writing-tutorials-and-blog-posts) - [Contributing to the wiki](#contributing-to-the-wiki) - [Creating and maintaining Coq packages](#creating-and-maintaining-coq-packages) - - [Distribution](#distribution) - - [Support](#support) + - [Distribution of Coq packages](#distribution-of-coq-packages) + - [Support for plugin and library authors](#support-for-plugin-and-library-authors) - [Standard libraries](#standard-libraries) - [Maintaining existing packages in coq-community](#maintaining-existing-packages-in-coq-community) - [Contributing to the editor support packages](#contributing-to-the-editor-support-packages) @@ -43,6 +43,7 @@ well. - [Reviewing pull requests](#reviewing-pull-requests) - [Merging pull requests](#merging-pull-requests) - [Additional notes for pull request reviewers and assignees](#additional-notes-for-pull-request-reviewers-and-assignees) + - [Joining / leaving maintainer teams](#joining--leaving-maintainer-teams) - [Core development team](#core-development-team) - [Release management](#release-management) - [Packaging Coq](#packaging-coq) @@ -60,6 +61,7 @@ well. - [Merge script dependencies](#merge-script-dependencies) - [Coqbot](#coqbot) - [Online forum and chat to talk to developers](#online-forum-and-chat-to-talk-to-developers) + - [Coq calls](#coq-calls) - [Coq remote working groups](#coq-remote-working-groups) - [Coq Users and Developers Workshops](#coq-users-and-developers-workshops) @@ -159,14 +161,14 @@ tools is great so that others can start building new things on top. Having an extensive and healthy package ecosystem will be key to the success of Coq. -#### Distribution #### +#### Distribution of Coq packages #### You can distribute your library or plugin through the [Coq package index][Coq-package-index]. Tools can be advertised on the [tools page][tools-website] of the Coq website, or the [tools page][tools-wiki] of the wiki. -#### Support #### +#### Support for plugin and library authors #### You can find advice and best practices about maintaining a Coq project on the [coq-community wiki][coq-community-wiki]. @@ -527,10 +529,20 @@ how you can anticipate the results of the CI before opening a PR. Such a failure can indicate either a bug in your branch, or a breaking change that you introduced voluntarily. All such breaking changes should be properly documented in the [user changelog][user-changelog]. -Furthermore, a backward-compatible fix should be found, and this fix -should be merged in the broken projects *before* your PR to the Coq -repository can be. You can use the same documentation as above to -learn about testing and fixing locally the broken libraries. +Furthermore, a backward-compatible fix should be found, properly +documented in the changelog when non-obvious, and this fix should be +merged in the broken projects *before* your PR to the Coq repository +can be. + +Note that once the breaking change is well understood, it should not +feel like it is your role to fix every project that is affected: as +long as reviewers have approved and are ready to integrate your +breaking change, you are entitled to (politely) request project +authors / maintainers to fix the breakage on their own, or help you +fix it. Obviously, you should leave enough time for this to happen +(you cannot expect a project maintainer to allocate time for this as +soon as you request it) and you should be ready to listen to more +feedback and reconsider the impact of your change. #### Understanding reviewers' feedback #### @@ -746,12 +758,15 @@ member of a team that was requested a review should self-assign the PR, and will act as its shepherd from then on. The PR assignee is responsible for making sure that all the proposed -changes have been reviewed by relevant maintainers, that change -requests have been implemented, that CI is passing, and eventually -will be the one who merges the PR. +changes have been reviewed by relevant maintainers (at least one +reviewer for each component that is significantly affected), that +change requests have been implemented, that CI is passing, and +eventually will be the one who merges the PR. *If you have already frequently contributed to a component, we would -be happy to have you join one of the maintainer teams.* +be happy to have you join one of the maintainer teams.* See the +[section below](#joining--leaving-maintainer-teams) on joining / +leaving maintainer teams. The complete list of maintainer teams is available [here][coq-pushers] (link only accessible to people who are already members of the Coq @@ -768,9 +783,20 @@ organization, because of a limitation of GitHub). they contributed to. However, reviewers may push small fixes to the PR branch to facilitate the PR integration. +- PRs are merged when there is consensus. Consensus is defined by an + explicit approval from at least one maintainer for each component + that is significantly affected and an absence of dissent. As soon + as a developer opposes a PR, it should not be merged without being + discussed first (usually in a call or working group). + +- Sometimes (especially for large or potentially controversial PRs), + it is a good practice to announce the intent to merge, one or + several days in advance, when unsure that everyone had a chance to + voice their opinion, or to finish reviewing the PR. + - Only PRs targetting the `master` branch can be merged by a maintainer. For PRs targetting a release branch, the assignee - should always be the RM. + should always be the release manager. - Before merging, the assignee must also select a milestone for the PR (see also Section [Release management](#release-management)). @@ -782,10 +808,6 @@ organization, because of a limitation of GitHub).  -- Sometimes, it is a good practice to announce the intent to merge one - or several days in advance when unsure that everyone had a chance to - voice their opinion, or to finish reviewing the PR. - - When a PR has [overlays][user-overlays], then: - the overlays that are backward-compatible (normally the case for @@ -798,6 +820,16 @@ organization, because of a limitation of GitHub). maintainers of the affected projects to ask them to merge the overlays). +#### Joining / leaving maintainer teams #### + +We are always happy to have more people involved in the PR reviewing +and merging process, so do not hesitate to propose yourself if you +already have experience on a component. + +Maintainers can leave teams at any time (and core members can also +join any team where they feel able to help) but you should always +announce it to other maintainers when you do join or leave a team. + ### Core development team ### The core developers are the active developers with a lengthy and @@ -1110,6 +1142,14 @@ Obviously, the issue tracker is also a good place to ask questions, especially if the development processes are unclear, or the developer documentation should be improved. +### Coq calls ### + +We try to gather every week for one hour through video-conference to +discuss current and urgent matters. When longer discussions are +needed, topics are left out for the next working group. See the +[wiki][wiki-calls] for more information about Coq calls, as well as +notes of past ones. + ### Coq remote working groups ### We semi-regularly (up to every month) organize remote working groups, @@ -1219,6 +1259,7 @@ can be found [on the wiki][wiki-CUDW]. [user-changelog]: doc/changelog [user-overlays]: dev/ci/user-overlays [wiki]: https://github.com/coq/coq/wiki +[wiki-calls]: https://github.com/coq/coq/wiki/Coq-Calls [wiki-CUDW]: https://github.com/coq/coq/wiki/CoqImplementorsWorkshop [wiki-WG]: https://github.com/coq/coq/wiki/Coq-Working-Groups [YouTube]: https://www.youtube.com/channel/UCbJo6gYYr0OF18x01M4THdQ |