Merge PR #11499: Clarify expectations for overlay creation

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: ejgallego

2 files changed, 27 insertions, 22 deletions

diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 9ed7180807..6a740b9033 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.