diff options
Diffstat (limited to 'dev/doc/MERGING.md')
| -rw-r--r-- | dev/doc/MERGING.md | 72 |
1 files changed, 43 insertions, 29 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 3a2df6a81..c0cd9c8cd 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -1,17 +1,17 @@ # Merging changes in Coq -This document describes how patches (submitted as pull requests -on the `master` branch) should be -merged into the main repository (https://github.com/coq/coq). +This document describes how patches, submitted as pull requests (PRs) on the +`master` branch, 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 +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 the principal -maintainer for a review. If the pull request touches several parts, all the +When a PR is submitted, GitHub will automatically ask the principal +maintainer for a review. If the PR touches several parts, all the corresponding principal maintainers will be asked for a review. Maintainers are never assigned as reviewer on their own PRs. @@ -43,17 +43,48 @@ A maintainer is expected to be reasonably reactive, but no specific timeframe is given for reviewing. (*) In case a component is touched in a trivial way (adding/removing one file in -a `Makefile`, etc), or by applying a systematic process (global renaming, -deprecationg propagation, etc) that has been reviewed globally, the assignee can +a `Makefile`, etc), or by applying a systematic refactoring process (global +renaming for instance) that has been reviewed globally, the assignee can say in a comment they think a review is not required and proceed with the merge. +### Breaking changes + +If the PR breaks compatibility of some external projects in CI, then fixes to +those external projects should have been prepared (cf. the relevant sub-section +in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested +with these fixes thanks to ["overlays"](../ci/user-overlays/README.md). + +Moreover the PR must absolutely update the [`CHANGES`](../../CHANGES) file. + +If overlays are missing, ask the author to prepare them and label the PR with +the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label. + +When fixes are ready, there are two cases to consider: + +- For patches that are backward compatible (best scenario), you should get the + external project maintainers to integrate them before merging the PR. +- For patches that are not backward compatible (which is often the case when + patching plugins after an update to the Coq API), you can proceed to merge + the PR and then notify the external project maintainers they can merge the + patch. + ## 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). +[merge script](../tools/merge-pr.sh). + +When CI has a few failures which look spurious, restarting the corresponding +jobs is a good way of ensuring this was indeed the case. +To restart a job on Travis, you should connect using your GitHub account; +being part of the Coq organization on GitHub should give you the permission +to do so. +To restart a job on GitLab CI, you should sign into GitLab (this can be done +using a GitHub account); if you are part of the +[Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry" +button; otherwise, send a request to join the organization. When the PR has conflicts, the assignee can either: - ask the author to rebase the branch, fixing the conflicts @@ -70,7 +101,7 @@ To merge the PR proceed in the following way ``` $ git checkout master $ git pull -$ dev/tools/merge-pr XXXX +$ dev/tools/merge-pr.sh XXXX $ git push upstream ``` where `XXXX` is the number of the PR to be merged and `upstream` is the name @@ -89,29 +120,12 @@ DON'T USE the GitHub interface for merging, since it will prevent the automated backport script from operating properly, generates bad commit messages, and a messy history when there are conflicts. -### What to do if the PR has overlays - -If the PR breaks compatibility of some developments in CI, then the author must -have prepared overlays for these developments (see [`dev/ci/README.md`](/dev/ci/README.md)) -and the PR must absolutely update the `CHANGES` file. - -There are two cases to consider: - -- If the patch is backward compatible (best scenario), then you should get - upstream maintainers to integrate it before merging the PR. -- If the patch is not backward compatible (which is often the case when - patching plugins after an update to the Coq API), then you can proceed to - merge the PR and then notify upstream they can merge the patch. This is a - less preferable scenario because it is probably going to create - spurious CI failures for unrelated PRs. - ### Merge script dependencies The merge script passes option `-S` to `git merge` to ensure merge commits are signed. Consequently, it depends on the GnuPG command utility being -installed and a GPG key being available. Here is a short tutorial to -creating your own GPG key: -<https://ekaia.org/blog/2009/05/10/creating-new-gpgkey/> +installed and a GPG key being available. Here is a short documentation on +how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/. The script depends on a few other utilities. If you are a Nix user, the simplest way of getting them is to run `nix-shell` first. |