Clarify expectations for overlays in contributing guide and CI doc.

Contributors are *not* required to prepare all the patches by
themselves.  They can request help from project authors, who should be
ready to take part in this.

Also, finish replacing "development" by the more appropriate word
"project".

3 files changed, 41 insertions, 26 deletions

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 6a72b68af0..7656998a51 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -527,10 +527,20 @@ how you can anticipate the results of the CI before opening a PR.
 Such a failure can indicate either a bug in your branch, or a breaking
 change that you introduced voluntarily.  All such breaking changes
 should be properly documented in the [user changelog][user-changelog].
-Furthermore, a backward-compatible fix should be found, and this fix
-should be merged in the broken projects *before* your PR to the Coq
-repository can be.  You can use the same documentation as above to
-learn about testing and fixing locally the broken libraries.
+Furthermore, a backward-compatible fix should be found, properly
+documented in the changelog when non-obvious, and this fix should be
+merged in the broken projects *before* your PR to the Coq repository
+can be.
+
+Note that once the breaking change is well understood, it should not
+feel like it is your role to fix every project that is affected: as
+long as reviewers have approved and are ready to integrate your
+breaking change, you are entitled to (politely) request project
+authors / maintainers to fix the breakage on their own, or help you
+fix it.  Obviously, you should leave enough time for this to happen
+(you cannot expect a project maintainer to allocate time for this as
+soon as you request it) and you should be ready to listen to more
+feedback and reconsider the impact of your change.
 
 #### Understanding reviewers' feedback ####
 
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 9ed7180807..dba3d38c6c 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -43,9 +43,10 @@ See also [`test-suite/README.md`](../../test-suite/README.md) for information ab
 ### 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. There is experimental support for an improved workflow, see
-[the next section](#experimental-automatic-overlay-creation-and-building), below
+prepare a patch (or ask someone —possibly the project author— to
+prepare a patch) to fix the project. There is experimental support for
+an improved workflow, see [the next
+section](#experimental-automatic-overlay-creation-and-building), below
 are the steps to manually prepare a patch:
 
 1. Fork the external project, create a new branch, push a commit adapting
diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md
index 06b617d4c1..6649820f22 100644
--- a/dev/ci/README-users.md
+++ b/dev/ci/README-users.md
@@ -1,36 +1,40 @@
 Information for external library / Coq plugin authors
 -----------------------------------------------------
 
-You are encouraged to consider submitting your development for addition to
+You are encouraged to consider submitting your project for addition to
 Coq's CI. This means that:
 
-- Any time that a proposed change is breaking your development, Coq developers
-  will send you patches to adapt it or, at the very least, will work with you
-  to see how to adapt it.
+- Any time that a proposed change is breaking your project, Coq
+  developers and contributors will send you patches to adapt it or
+  will explain how to adapt it and work with you to ensure that you
+  manage to do it.
 
 On the condition that:
 
-- At the time of the submission, your development works with Coq's
+- At the time of the submission, your project works with Coq's
   `master` branch.
 
-- Your development is publicly available in a git repository and we can easily
+- Your project is publicly available in a git repository and we can easily
   send patches to you (e.g. through pull / merge requests).
 
 - You react in a timely manner to discuss / integrate those patches.
+  When seeking your help for preparing such patches, we will accept
+  that it takes longer than when we are just requesting to integrate a
+  simple (and already fully prepared) patch.
 
 - You do not push, to the branches that we test, commits that haven't been
   first tested to compile with the corresponding branch(es) of Coq.
 
-  For that, we recommend setting a CI system for you development, see
+  For that, we recommend setting a CI system for you project, see
   [supported CI images for Coq](#supported-ci-images-for-coq) below.
 
-- You maintain a reasonable build time for your development, or you provide
+- You maintain a reasonable build time for your project, or you provide
   a "lite" target that we can use.
 
 In case you forget to comply with these last three conditions, we would reach
-out to you and give you a 30-day grace period during which your development
+out to you and give you a 30-day grace period during which your project
 would be moved into our "allow failure" category. At the end of the grace
-period, in the absence of progress, the development would be removed from our
+period, in the absence of progress, the project would be removed from our
 CI.
 
 ### Timely merging of overlays
@@ -47,7 +51,7 @@ these kind of merges.
 
 ### OCaml and plugin-specific considerations
 
-Developments that link against Coq's OCaml API [most of them are known
+Projects that link against Coq's OCaml API [most of them are known
 as "plugins"] do have some special requirements:
 
 - Coq's OCaml API is not stable. We hope to improve this in the future
@@ -65,7 +69,7 @@ as "plugins"] do have some special requirements:
   uses. In particular, warnings that are considered fatal by the Coq
   developers _must_ be also fatal for plugin CI code.
 
-### Add your development by submitting a pull request
+### Add your project by submitting a pull request
 
 Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding
 variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the
@@ -75,7 +79,7 @@ Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an
 example. **Do not hesitate to submit an incomplete pull request if you need
 help to finish it.**
 
-You may also be interested in having your development tested in our
+You may also be interested in having your project tested in our
 performance benchmark. Currently this is done by providing an OPAM package
 in https://github.com/coq/opam-coq-archive and opening an issue at
 https://github.com/coq/coq-bench/issues.
@@ -83,13 +87,13 @@ https://github.com/coq/coq-bench/issues.
 ### Recommended branching policy.
 
 It is sometimes the case that you will need to maintain a branch of
-your development for particular Coq versions. This is in fact very
-likely if your development includes a Coq ML plugin.
+your project for particular Coq versions. This is in fact very likely
+if your project includes a Coq ML plugin.
 
-We thus recommend a branching convention that mirrors Coq's branching
-policy. Then, you would have a `master` branch that follows Coq's
-`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so
-on.
+For such projects, we recommend a branching convention that mirrors
+Coq's branching policy. Then, you would have a `master` branch that
+follows Coq's `master`, a `v8.8` branch that works with Coq's `v8.8`
+branch and so on.
 
 This convention will be supported by tools in the future to make some
 developer commands work more seamlessly.