diff options
Diffstat (limited to 'dev/ci/README.md')
| -rw-r--r-- | dev/ci/README.md | 38 |
1 files changed, 27 insertions, 11 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index dee3d2aff7..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. +See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. -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. +### Breaking changes -See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. +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 ------------------------------ @@ -141,7 +154,6 @@ no OCaml warnings build Coq in parallel with other tests. ### GitLab and Windows - If your repository has access to runners tagged `windows`, setting the secret variable `WINDOWS` to `enabled` will add jobs building Windows versions of Coq (32bit and 64bit). @@ -155,6 +167,10 @@ System and opam packages are installed in a Docker image. The image is automatically built and uploaded to your GitLab registry, and is loaded by subsequent jobs. +**IMPORTANT**: When updating Coq's CI docker image, you must modify +the `CACHEKEY` variable in `.gitlab-ci.yml`, `.circleci/config.yml`, +and `Dockerfile`. + The Docker building job reuses the uploaded image if it is available, but if you wish to save more time you can skip the job by setting `SKIP_DOCKER` to `true`. |