Complete rewrite of the documentation of overlays after Jim's additional comments.

[ci skip]

3 files changed, 62 insertions, 47 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 8cbe8fc33..aec2dfe0a 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -1,18 +1,17 @@
 # Add overlays for your pull requests in this directory
 
-When your pull request breaks an external development we test in our CI, you
-must prepare a patch (or ask someone to prepare a patch) to fix this development.
-Backward compatible patches are to be preferred, especially on libraries (it is
-harder to make backward compatible patches for plugins).
-
-Once you have a patched version, you can add an overlay to your pull request:
-this is a file which defines where to look for the patched version so that
-testing is possible. It changes the value of some variables from
-[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh) (generally both the
-`_CI_BRANCH` and the `_CI_GITURL` variables of a given development at once).
-
-The file contains very simple logic to test the pull request number or branch
-name and apply it only in this case.
+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.
+
+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
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 14d30517c..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.
@@ -47,6 +47,27 @@ 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,24 +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/user-overlays/README.md`](/dev/ci/user-overlays/README.md) for
-detailed explanations of what this is)
-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