1 files changed, 136 insertions, 0 deletions
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)).