diff options
| author | Emilio Jesus Gallego Arias | 2018-11-18 17:39:57 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-24 13:16:00 +0100 |
| commit | c8dd2b51e413ae1522b6278e36b5e56e0f9a5585 (patch) | |
| tree | de0c04d460b999d0520327cf9bdab7968d9e7e28 /dev/ci | |
| parent | 991790c8135cf3073907fda3baadc9718419f173 (diff) | |
[ci] [doc] Note about `overlay-maintainers` team.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/README-developers.md | 4 | ||||
| -rw-r--r-- | dev/ci/README-users.md | 12 |
2 files changed, 14 insertions, 2 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 8cb1a0edef..54da7a7cd3 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -72,7 +72,7 @@ Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) fil If you break external projects that are hosted on GitHub, you can use the `create-overlays.sh` script to automatically perform most of the -above step. In order to do so, call the script as: +above steps. In order to do so, call the script as: ``` ./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac ``` @@ -81,7 +81,7 @@ number. The script will: - checkout the contributions and prepare the branch/remote so you can just commit the fixes and push, -- add the corresponding overlay file in `dev/ci/user-overlays` +- add the corresponding overlay file in `dev/ci/user-overlays`. For problems related to ML-plugins, if you use `dune build` to build Coq, it will actually be aware of the broken contributions and perform diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index 2b400f4136..f606f43fd5 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -33,6 +33,18 @@ 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 CI. +### Timely merging of overlays + +A pitfall of the current CI setup is that when a breaking change is +merged in Coq upstream, CI for your contrib will be broken until you +merge the corresponding pull request with the fix for your contribution. + +As of today, you have to worry about synchronizing with Coq upstream +every once in a while; we hope we will improve this in the future by +using [coqbot](https://github.com/coq/bot); meanwhile, a workaround is +to give merge permissions to someone from the Coq team as to help with +these kind of merges. + ### Add your development by submitting a pull request Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding |