From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- dev/doc/MERGING.md | 136 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 136 insertions(+) create mode 100644 dev/doc/MERGING.md (limited to 'dev/doc/MERGING.md') diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md new file mode 100644 index 00000000..000f21c2 --- /dev/null +++ b/dev/doc/MERGING.md @@ -0,0 +1,136 @@ +# Merging changes in 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 +system, two owners. One is the principal maintainer of the component, the other +is the secondary maintainer. + +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. + +If a principal maintainer submits a PR that changes the component they own, they +must assign the secondary maintainer as reviewer. They should also do it if they +know they are not available to do the review. + +## Reviewing + +When 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 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. + +(*) In case a component is touched in a trivial way (adding/removing one file in +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.md`](../../CHANGES.md) 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](../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 +- warn the author that they are going to rebase the branch, and push to the + branch directly + +In both cases, CI should be run again. + +In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix +the conflicts in the merge commit (following the same steps as below), and push +to `master` directly. Don't use the GitHub interface to fix these conflicts. + +To merge the PR proceed in the following way +``` +$ git checkout master +$ git pull +$ 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 +of your remote pointing to `git@github.com:coq/coq.git`. +Note that you are only supposed to merge PRs into `master`. PRs should rarely +target the stable branch, but when it is the case they are the responsibility +of the release manager. + +This script conducts various checks before proceeding to merge. Don't bypass them +without a good reason to, and in that case, write a comment in the PR thread to +explain the reason. + +Maintainers MUST NOT merge their own patches. + +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. + +### 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 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. + +**Note for homebrew (MacOS) users:** it has been reported that installing GnuPG +is not out of the box. Installing explicitly "pinentry-mac" seems important for +typing of passphrase to work correctly (see also this +[Stack Overflow Q-and-A](https://stackoverflow.com/questions/39494631/gpg-failed-to-sign-the-data-fatal-failed-to-write-commit-object-git-2-10-0)). -- cgit v1.2.3