Merge PR #12113: Contributing guide improvements

Reviewed-by: ejgallego

1 files changed, 126 insertions, 84 deletions

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 201d740073..3582d18cf6 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -30,17 +30,18 @@ well.
   - [Helping triage existing issues](#helping-triage-existing-issues)
 - [Code changes](#code-changes)
   - [Using GitHub pull requests](#using-github-pull-requests)
+    - [Fixing bugs and performing small changes](#fixing-bugs-and-performing-small-changes)
+    - [Proposing large changes: Coq Enhancement Proposals](#proposing-large-changes-coq-enhancement-proposals)
+    - [Seeking early feedback on work-in-progress](#seeking-early-feedback-on-work-in-progress)
   - [Taking feedback into account](#taking-feedback-into-account)
     - [Understanding automatic feedback](#understanding-automatic-feedback)
     - [Understanding reviewers' feedback](#understanding-reviewers-feedback)
     - [Fixing your branch](#fixing-your-branch)
   - [Improving the official documentation](#improving-the-official-documentation)
   - [Contributing to the standard library](#contributing-to-the-standard-library)
-  - [Fixing bugs and performing small changes](#fixing-bugs-and-performing-small-changes)
-  - [Proposing large changes: Coq Enhancement Proposals](#proposing-large-changes-coq-enhancement-proposals)
-  - [Collaborating on a pull request](#collaborating-on-a-pull-request)
 - [Becoming a maintainer](#becoming-a-maintainer)
   - [Reviewing pull requests](#reviewing-pull-requests)
+    - [Collaborating on a pull request](#collaborating-on-a-pull-request)
   - [Merging pull requests](#merging-pull-requests)
     - [Additional notes for pull request reviewers and assignees](#additional-notes-for-pull-request-reviewers-and-assignees)
     - [Joining / leaving maintainer teams](#joining--leaving-maintainer-teams)
@@ -443,6 +444,72 @@ several months after your PR is merged).  That said, you can start
 using the latest Coq `master` branch to take advantage of all the new
 features, improvements, and fixes.
 
+#### Fixing bugs and performing small changes ####
+
+Before fixing a bug, it is best to check that it was reported before:
+
+- If it was already reported and you intend to fix it, self-assign the
+  issue (if you have the permission), or leave a comment marking your
+  intention to work on it (and a contributor with write-access may
+  then assign the issue to you).
+
+- If the issue already has an assignee, you should check with them if
+  they still intend to work on it.  If the assignment is several
+  weeks, months, or even years (!) old, there are good chances that it
+  does not reflect their current priorities.
+
+- If the bug has not been reported before, it can be a good idea to
+  open an issue about it, while stating that you are preparing a fix.
+  The issue can be the place to discuss about the bug itself while the
+  PR will be the place to discuss your proposed fix.
+
+It is generally a good idea to add a regression test to the
+test-suite. See the test-suite [README][test-suite-README] for how to
+do so.
+
+Small fixes do not need any documentation, or changelog update.  New,
+or updated, user-facing features, and major bug fixes do.  See above
+on how to contribute to the documentation, and the README in
+[`doc/changelog`][user-changelog] for how to add a changelog entry.
+
+#### Proposing large changes: Coq Enhancement Proposals ####
+
+You are always welcome to open a PR for a change of any size.
+However, you should be aware that the larger the change, the higher
+the chances it will take very long to review, and possibly never get
+merged.
+
+So it is recommended that before spending a lot of time coding, you
+seek feedback from maintainers to see if your change would be
+supported, and if they have recommendations about its implementation.
+You can do this informally by opening an issue, or more formally by
+producing a design document as a [Coq Enhancement Proposal][CEP].
+
+Another recommendation is that you do not put several unrelated
+changes in the same PR (even if you produced them together).  In
+particular, make sure you split bug fixes into separate PRs when this
+is possible.  More generally, smaller-sized PRs, or PRs changing less
+components, are more likely to be reviewed and merged promptly.
+
+#### Seeking early feedback on work-in-progress ####
+
+You should always feel free to open your PR before the documentation,
+changelog entry and tests are ready.  That's the purpose of the
+checkboxes in the PR template which you can leave unticked.  This can
+be a way of getting reviewers' approval before spending time on
+writing the documentation (but you should still do it before your PR
+can be merged).
+
+If even the implementation is not ready but you are still looking for
+early feedback on your code changes, please use the [draft
+PR](#draft-pull-requests) mechanism.
+
+If you are looking for feedback on the design of your change, rather
+than on its implementation, then please refrain from opening a PR.
+You may open an issue to start a discussion, or create a [Coq
+Enhancement Proposal][CEP] if you have a clear enough view of the
+design to write a document about it.
+
 ### Taking feedback into account ###
 
 #### Understanding automatic feedback ####
@@ -644,59 +711,35 @@ Add coqdoc comments to extend the [standard library
 documentation][stdlib-doc].  See the [coqdoc
 documentation][coqdoc-documentation] to learn more.
 
-### Fixing bugs and performing small changes ###
-
-Before fixing a bug, it is best to check that it was reported before:
-
-- If it was already reported and you intend to fix it, self-assign the
-  issue (if you have the permission), or leave a comment marking your
-  intention to work on it (and a contributor with write-access may
-  then assign the issue to you).
-
-- If the issue already has an assignee, you should check with them if
-  they still intend to work on it.  If the assignment is several
-  weeks, months, or even years (!) old, there are good chances that it
-  does not reflect their current priorities.
-
-- If the bug has not been reported before, it can be a good idea to
-  open an issue about it, while stating that you are preparing a fix.
-  The issue can be the place to discuss about the bug itself while the
-  PR will be the place to discuss your proposed fix.
-
-In any case, feel free to just ignore the recommendation above, and
-jump ahead and open a PR with your fix.  If it is not yet complete, do
-not hesitate to open a [*draft PR*][GitHub-draft-PR] to get early
-feedback, and talk to developers on [Gitter][].
-
-It is generally a good idea to add a regression test to the
-test-suite. See the test-suite [README][test-suite-README] for how to
-do so.
-
-Small fixes do not need any documentation, or changelog update.  New,
-or updated, user-facing features, and major bug fixes do.  See above
-on how to contribute to the documentation, and the README in
-[`doc/changelog`][user-changelog] for how to add a changelog entry.
+## Becoming a maintainer ##
 
-### Proposing large changes: Coq Enhancement Proposals ###
+### Reviewing pull requests ###
 
-You are always welcome to open a PR for a change of any size.
-However, you should be aware that the larger the change, the higher
-the chances it will take very long to review, and possibly never get
-merged.
+You can start reviewing PRs as soon as you feel comfortable doing so
+(anyone can review anything, although some designated reviewers
+will have to give a final approval before a PR can be merged, as is
+explained in the next sub-section).
 
-So it is recommended that before spending a lot of time coding, you
-seek feedback from maintainers to see if your change would be
-supported, and if they have recommendations about its implementation.
-You can do this informally by opening an issue, or more formally by
-producing a design document as a [Coq Enhancement Proposal][CEP].
+Reviewers should ensure that the code that is changed or introduced is
+in good shape and will not be a burden to maintain, is unlikely to
+break anything, or the compatibility-breakage has been identified and
+validated, includes documentation, changelog entries, and test files
+when necessary.  Reviewers can use labels, or change requests to
+further emphasize what remains to be changed before they can approve
+the PR.  Once reviewers are satisfied (regarding the part they
+reviewed), they should formally approve the PR, possibly stating what
+they reviewed.
 
-Another recommendation is that you do not put several unrelated
-changes in the same PR (even if you produced them together).  In
-particular, make sure you split bug fixes into separate PRs when this
-is possible.  More generally, smaller-sized PRs, or PRs changing less
-components, are more likely to be reviewed and merged promptly.
+That being said, reviewers should also make sure that they do not make
+the contributing process harder than necessary: they should make it
+clear which comments are really required to perform before approving,
+and which are just suggestions.  They should strive to reduce the
+number of rounds of feedback that are needed by posting most of their
+comments at the same time.  If they are opposed to the change, they
+should clearly say so from the beginning to avoid the contributor
+spending time in vain.
 
-### Collaborating on a pull request ###
+#### Collaborating on a pull request ####
 
 Beyond making suggestions to a PR author during the review process,
 you may want to collaborate further by checking out the code, making
@@ -721,42 +764,14 @@ else), this should be reflected by adding ["Co-authored-by:"
 tags][GitHub-co-authored-by] at the end of the commit message.  The
 line should contain the co-author name and committer e-mail address.
 
-## Becoming a maintainer ##
-
-### Reviewing pull requests ###
-
-You can start reviewing PRs as soon as you feel comfortable doing so
-(anyone can review anything, although some designated reviewers
-will have to give a final approval before a PR can be merged, as is
-explained in the next sub-section).
-
-Reviewers should ensure that the code that is changed or introduced is
-in good shape and will not be a burden to maintain, is unlikely to
-break anything, or the compatibility-breakage has been identified and
-validated, includes documentation, changelog entries, and test files
-when necessary.  Reviewers can use labels, or change requests to
-further emphasize what remains to be changed before they can approve
-the PR.  Once reviewers are satisfied (regarding the part they
-reviewed), they should formally approve the PR, possibly stating what
-they reviewed.
-
-That being said, reviewers should also make sure that they do not make
-the contributing process harder than necessary: they should make it
-clear which comments are really required to perform before approving,
-and which are just suggestions.  They should strive to reduce the
-number of rounds of feedback that are needed by posting most of their
-comments at the same time.  If they are opposed to the change, they
-should clearly say so from the beginning to avoid the contributor
-spending time in vain.
-
 ### Merging pull requests ###
 
 Our [CODEOWNERS][] file associates a team of maintainers to each
-component.  When a PR is opened (or a draft PR is marked as ready for
-review), GitHub will automatically request reviews to maintainer teams
-of affected components.  As soon as it is the case, one available
-member of a team that was requested a review should self-assign the
-PR, and will act as its shepherd from then on.
+component.  When a PR is opened (or a [draft PR](#draft-pull-requests)
+is marked as ready for review), GitHub will automatically request
+reviews to maintainer teams of affected components.  As soon as it is
+the case, one available member of a team that was requested a review
+should self-assign the PR, and will act as its shepherd from then on.
 
 The PR assignee is responsible for making sure that all the proposed
 changes have been reviewed by relevant maintainers (at least one
@@ -1100,6 +1115,33 @@ interface to mark as read, save for later or mute threads.  You can
 also manage your GitHub web notifications using a tool such as
 [Octobox][].
 
+##### Draft pull requests #####
+
+[Draft PRs][GitHub-draft-PR] are a mechanism proposed by GitHub to
+open a pull request before it is ready for review.
+
+Opening a draft PR is a way of announcing a change and seeking early
+feedback without formally requesting maintainers' reviews.  Indeed,
+you should avoid cluttering our maintainers' review request lists
+before a change is ready on your side.
+
+When opening a draft PR, make sure to give it a descriptive enough
+title so that interested developers still notice it in their
+notification feed.  You may also advertise it by talking about it in
+our [developer chat][Gitter].  If you know which developer would be
+able to provide useful feedback to you, you may also ping them.
+
+###### Turning a PR into draft mode ######
+
+If a PR was opened as ready for review, but it turns out that it still
+needs work, it can be transformed into a draft PR.
+
+In this case, previous review requests won't be removed automatically.
+Someone with write access to the repository should remove them
+manually.  Afterwards, upon marking the PR as ready for review,
+someone with write access will have to manually add the review
+requests that were previously removed.
+
 #### GitLab documentation, tips and tricks ####
 
 We use GitLab mostly for its CI service.  The [Coq organization on