From c0dd7253faa83d1f3230e57071073df321a5e389 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 22 May 2018 11:09:58 +0200 Subject: Improve merging and overlay documentations. Clarification prompted by Jim Fehrle. [ci skip] --- dev/ci/user-overlays/README.md | 17 +++++++++++++++-- dev/doc/MERGING.md | 8 +++++--- 2 files changed, 20 insertions(+), 5 deletions(-) (limited to 'dev') diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index a7474e3248..3414a8786b 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 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). -The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`. +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. + +The name of your overlay file should be of the form +`five_digit_PR_number-GitHub_handle-branch_name.sh`. Example: `00669-maximedenes-ssr-merge.sh` containing diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index a466124c1c..14d30517cb 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -43,8 +43,8 @@ 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. ## Merging @@ -92,7 +92,9 @@ 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)) +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: -- cgit v1.2.3 From 87af4f4c41878bee5d02ab8560898c56611baa4c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 22 May 2018 12:59:05 +0200 Subject: Relax advice on the name of user-overlays following Gaëtan's suggestion. [ci skip] --- dev/ci/user-overlays/README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'dev') diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 3414a8786b..8cbe8fc339 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -14,8 +14,9 @@ testing is possible. It changes the value of some variables from 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 be of the form -`five_digit_PR_number-GitHub_handle-branch_name.sh`. +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 -- cgit v1.2.3 From bc5d403411f746831b99e4fd87b5eba1ded0560a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 24 May 2018 16:43:27 +0200 Subject: Complete rewrite of the documentation of overlays after Jim's additional comments. [ci skip] --- dev/ci/README.md | 35 ++++++++++++++++++++---------- dev/ci/user-overlays/README.md | 25 +++++++++++---------- dev/doc/MERGING.md | 49 ++++++++++++++++++++++-------------------- 3 files changed, 62 insertions(+), 47 deletions(-) (limited to 'dev') diff --git a/dev/ci/README.md b/dev/ci/README.md index ed3442e0db..697a160ca9 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 8cbe8fc339..aec2dfe0a6 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 14d30517cb..65457b63af 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 -- cgit v1.2.3