Merge PR #7574: Improve merging and overlay documentations.

3 files changed, 67 insertions, 36 deletions

diff --git a/dev/ci/README.md b/dev/ci/README.md
index ed3442e0d..697a160ca 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -107,19 +107,32 @@ there are some.
 
 You can also run one CI target locally (using `make ci-somedev`).
 
-Whenever your PR breaks tested developments, you should either adapt it
-so that it doesn't, or provide a branch fixing these developments (or at
-least work with the author of the development / other Coq developers to
-prepare these fixes). Then, add an overlay in
-[`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there)
-as part of your PR.
-
-The process to merge your PR is then to submit PRs to the external
-development repositories, merge the latter first (if the fixes are
-backward-compatible), and merge the PR on Coq then.
-
 See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite.
 
+### Breaking changes
+
+When your PR breaks an external project we test in our CI, you must prepare a
+patch (or ask someone to prepare a patch) to fix the project:
+
+1. Fork the external project, create a new branch, push a commit adapting
+   the project to your changes.
+2. Test your pull request with your adapted version of the external project by
+   adding an overlay file to your pull request (cf.
+   [`dev/ci/user-overlays/README.md`](/dev/ci/user-overlays/README.md)).
+3. Fixes to external libraries (pure Coq projects) *must* be backward
+   compatible (i.e. they should also work with the development version of Coq,
+   and the latest stable version). This will allow you to open a PR on the
+   external project repository to have your changes merged *before* your PR on
+   Coq can be integrated.
+
+   On the other hand, patches to plugins (projects linking to the Coq ML API)
+   can very rarely be made backward compatible and plugins we test will
+   generally have a dedicated branch per Coq version.
+   You can still open a pull request but the merging will be requested by the
+   developer who merges the PR on Coq. There are plans to improve this, cf.
+   [#6724](https://github.com/coq/coq/issues/6724).
+
+Moreover your PR must absolutely update the [`CHANGES`](/CHANGES) file.
 
 Advanced GitLab CI information
 ------------------------------
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index a7474e324..aec2dfe0a 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -1,8 +1,21 @@
 # Add overlays for your pull requests in this directory
 
-An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh).
+When your pull request breaks an external project we test in our CI and you
+have prepared a branch with the fix, you can add an "overlay" to your pull
+request to test it with the adapted version of the external project.
 
-The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`.
+An overlay is a file which defines where to look for the patched version so that
+testing is possible. It redefines some variables from
+[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh):
+give the name of your branch using a `_CI_BRANCH` variable and the location of
+your fork using a `_CI_GITURL` variable.
+
+Moreover, the file contains very simple logic to test the pull request number
+or branch name and apply it only in this case.
+
+The name of your overlay file should start with a five-digit pull request
+number, followed by a dash, anything (for instance your GitHub nickname
+and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`).
 
 Example: `00669-maximedenes-ssr-merge.sh` containing
 
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index a466124c1..65457b63a 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -1,8 +1,8 @@
 # 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
 
@@ -10,8 +10,8 @@ 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,10 +43,31 @@ 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](/dev/ci/README.md#Breaking-changes) and the PR can be tested
+with these fixes thanks to ["overlays"](/dev/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
@@ -89,22 +110,6 @@ 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