1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
# Add overlays for your pull requests in this directory
_Overlays_ let you test pull requests that break the base version of
external projects by applying PRs of the external project during CI
testing (1 PR per broken external project). Once Coq CI's tests of the
external projects pass, the Coq PR can be merged, then the assignee must
ask the external projects to merge their PRs (for example by commenting
in the external PRs). External projects are then expected to merge their
PRs promptly.
An overlay file specifies the external PRs that should be applied during CI.
A single file can cover multiple external projects. Create your
overlay file in the `dev/ci/user-overlays` directory.
The name of the overlay file should start with a five-digit pull request
number, followed by a dash, anything (by convention, your GitHub nickname
and the branch name), then an `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`).
The file must contain a call to the `overlay` function for each
affected external project:
```
overlay <project> <giturl> <ref> <prnumber> [<prbranch>]
```
Each call creates an overlay for `project` using a given `giturl` and
`ref` which is active for `prnumber` or `prbranch` (`prbranch` defaults
to `ref`).
For example, an overlay for the project `elpi` that uses the branch `noinstance`
from the fork of `SkySkimmer` and is active for pull request `13128`:
```
overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance 13128
```
The github URL and base branch name for each external project are listed in
[`ci-basic-overlay.sh`](../ci-basic-overlay.sh). For example, the entry for
`elpi` is
```
project elpi "https://github.com/LPCIC/coq-elpi" "coq-master"
```
But substitute the name of your fork into the URL, e.g. `SkySkimmer/coq-elpi`
rather than `LPCIC/coq-elpi`. Use `#` to mark any comments.
If the branch name in the external project differs from the Coq branch name,
include the external branch name as `[prbranch]` to apply it when you run
the test suite locally, e.g. `make ci-elpi`.
Overlay files can be created automatically using the script
[`create_overlays.sh`](../../tools/create_overlays.sh).
### Branching conventions
We suggest you use the convention of identical branch names for the
Coq branch and the CI project branch used in the overlay. For example,
if your Coq PR is in your branch `more_efficient_tc` and
breaks `ltac2`, we suggest you create an `ltac2` overlay with a branch
named `more_efficient_tc`.
### Typical workflow
- Observe that your changes breaks some external projects in CI
- Compile your PR.
- For each broken project, run `make <job name>`, e.g. `make ci-elpi`,
which checks out, builds and runs the project in the
`_build_ci/<job name>` directory. (Make sure the `_build_vo`
directory does not exist in your source tree. Or, soon, run
`make -f Makefile.dune ci-foo`.)
- Make necessary changes, then rerun the script to verify they work.
- From the `<job name>` subdirectory, commit your changes to a new
branch, based on the base branch name listed in `ci-basic-overlay.sh`,
for example `coq-master` for elpi.
- If necessary, fork the external project from the project's github page.
(Only needs to be done once, ever.)
- Push to the external project and create a new PR. Make sure you pick
the correct base branch in the github GUI for the comparison
(e.g. `coq-master` for elpi).
- Create the overlay file, add to your Coq PR, push the updated version and
verify that the external projects now pass.
- When your PR is merged, the assignee notifies the maintainers of the
external project to merge the changes you submitted. This should happen
promptly; the external project's CI will fail until the change is merged.
- Beer.
|
