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 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) (limited to 'dev/ci') 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 -- 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/ci') 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 ++++++++++++------------- 2 files changed, 36 insertions(+), 24 deletions(-) (limited to 'dev/ci') 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 -- cgit v1.2.3