1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
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.
|
