diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-16 18:44:01 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-19 19:49:57 +0100 |
commit | 57877caba02e8e9a950f5302b887970dcb9712a7 (patch) | |
tree | 449cac722a18aea7ba53325a1445547f2319f517 /dev/doc/MERGING.md | |
parent | f21deb6c861b359f0d3bf8b170d277cfa0d80171 (diff) |
Describe new merging process.
Diffstat (limited to 'dev/doc/MERGING.md')
-rw-r--r-- | dev/doc/MERGING.md | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md new file mode 100644 index 000000000..df366a978 --- /dev/null +++ b/dev/doc/MERGING.md @@ -0,0 +1,54 @@ +# Merging changes in Coq + +This document describes how patches (submitted as Pull Requests) should be +merged into the main repository (https://github.com/coq/coq). + +## Code owners + +The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the +system, two owners. One is the principal maintainer of the component, the other +is the secondary maintainer. + +When a pull request is submitted, GitHub will automatically ask these two +maintainers for a review. If the pull request touches several parts, all the +corresponding maintainers will be asked for a review. + +Maintainers are never assigned as reviewer on their own PRs. + +## Reviewing + +When principal maintainers receive a review request, they are expected to: + +* Put their name in the assignee field, if they are in charge of the component + that is the main target of the patch (or if they are the only principal + maintainer asked to review the PR). +* Review the PR, approve it or request changes. +* If they are the assignee, check if all reviewers approved the PR. If not, + regularly ping the author (if changes should be implemented) or the reviewers + (if reviews are missing). The assignee ensures that any requests for more + discussion have been granted. When the discussion has converged and all + reviewers have approved the PR, the assignee is expected to follow the merging + process described below. + +In all cases, maintainers can delegate reviews to the other maintainer of the +same component, except if it would lead to a maintainer reviewing their own +patch. + +A maintainer is expected to be reasonably reactive, but no specific timeframe is +given for reviewing. + +## Merging + +Once all reviewers approved the PR, the assignee is expected to check that CI +completed without relevant failures, and that the PR comes with appropriate +documentation and test cases. If not, they should leave a comment on the PR and +put the approriate label. Otherwise, they are expected to merge the PR using the +[merge script](/dev/tools/merge-pr.sh). + +The command to be used is: +``` +$ dev/tools/merge-pr XXXX +``` +where `XXXX` is the number of the PR to be merged. This operation should be followed by a push. + +Maintainers MUST NOT merge their own patches. |