README.md 8.93 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
# Shared Iris CI
Ralf Jung's avatar
Ralf Jung committed
2

Ralf Jung's avatar
Ralf Jung committed
3
4
This repository contains the shared Iris CI. It contains common code for Iris
projects' CI.
Ralf Jung's avatar
Ralf Jung committed
5

Ralf Jung's avatar
Ralf Jung committed
6
Projects automatically use the latest commit of *some branch* for their CI, so
Ralf Jung's avatar
Ralf Jung committed
7
8
9
10
branches should remain reasonably compatible.  Every branch here comes with a
corresponding branch [in the Docker repo](https://github.com/RalfJung/opam-ci),
providing the Docker image that should be used.  Currently, we have the
following branches:
Ralf Jung's avatar
Ralf Jung committed
11

Ralf Jung's avatar
Ralf Jung committed
12
* [`opam2`](https://gitlab.mpi-sws.org/FP/iris-ci/tree/opam2), using opam 2.0.
Ralf Jung's avatar
Ralf Jung committed
13

Ralf Jung's avatar
Ralf Jung committed
14
15
16
Pushing to `master` here will not be picked up by the projects, always remember
to also push to the right branch!

Ralf Jung's avatar
Ralf Jung committed
17
18
## How to configure CI for your project

Ralf Jung's avatar
Ralf Jung committed
19
20
Inside your project, create a `.gitlab-ci.yml` with the following prelude,
substituting `\REPO` for the name of the repository (e.g. `iris/stdpp`):
Ralf Jung's avatar
Ralf Jung committed
21

Ralf Jung's avatar
Ralf Jung committed
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
```
image: ralfjung/opam-ci:opam2

stages:
  - build

variables:
  CPU_CORES: "10"

.template: &template
  stage: build
  tags:
  - fp
  script:
  - git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
  - ci/buildjob
  cache:
    key: "$CI_JOB_NAME"
    paths:
41
    - _opam/
Ralf Jung's avatar
Ralf Jung committed
42
  only:
Ralf Jung's avatar
Ralf Jung committed
43
44
  - master@\REPO
  - /^ci/@\REPO
Ralf Jung's avatar
Ralf Jung committed
45
46
47
  except:
  - triggers
  - schedules
Ralf Jung's avatar
Ralf Jung committed
48
  - api
Ralf Jung's avatar
Ralf Jung committed
49
50
51

## Build jobs
```
Ralf Jung's avatar
Ralf Jung committed
52

Ralf Jung's avatar
Ralf Jung committed
53
54
55
56
This sets up a template that we will use for the jobs.  The `tags` determine the
CI runner that will pick up these jobs; `only` and `except` make this run only
when things get pushed to master and branches whose name start with `ci` and not
when the pipeline gets triggered though the API or an automatic schedule.  See
Ralf Jung's avatar
Ralf Jung committed
57
58
59
[the GitLab CI documentation][gitlab-ci] for more information.

[gitlab-ci]: https://docs.gitlab.com/ce/ci/yaml/README.html
Ralf Jung's avatar
Ralf Jung committed
60
61

Below this, you can configure your build jobs.  A normal job looks like this:
Ralf Jung's avatar
Ralf Jung committed
62

Ralf Jung's avatar
Ralf Jung committed
63
```
Ralf Jung's avatar
Ralf Jung committed
64
build-coq.8.10.1:
Ralf Jung's avatar
Ralf Jung committed
65
66
  <<: *template
  variables:
Ralf Jung's avatar
Ralf Jung committed
67
    OPAM_PINS: "coq version 8.10.1"
Ralf Jung's avatar
Ralf Jung committed
68
```
Ralf Jung's avatar
Ralf Jung committed
69

Ralf Jung's avatar
Ralf Jung committed
70
71
72
This builds your project against Coq 8.8.2.  The first line determines the job
name shown in GitLab.  The second line imports the template we defined in the
prelude.  The last two lines configure the job; `OPAM_PINS` sets up the pins for
Ralf Jung's avatar
Ralf Jung committed
73
74
75
the environment that the job will be built in.  You can add `CI_COQCHK: "1"` to
run `coqchk` after the build is done; be aware that can be very slow and hence
use a lot of CI time.
Ralf Jung's avatar
Ralf Jung committed
76
77
78

See [buildjob](buildjob) for a list of available configuration variables.  Some
of them require a secret or a key to be configured for the project; these are
Ralf Jung's avatar
Ralf Jung committed
79
80
81
82
83
84
85
86
passed in as "Environment variables" setup in the GitLab UI.

The most versatile variable is `OPAM_PINS`, which configures the packages to pin
before installing dependencies: Each package can be:
- a group of three list elements: `PACKAGE KIND TARGET`.
- a single element denoting a git repository, starting with `git+https://`.

Below, we describe some of the things that are common amongst Iris build jobs.
Ralf Jung's avatar
Ralf Jung committed
87
88
89
90

## Nightly builds

To make sure that a project keeps working as we update Iris, we can set up
Ralf Jung's avatar
Ralf Jung committed
91
92
93
nightly builds against the latest Iris version, and often we pin that to a
*branch* of Coq to make sure we keep working with the next patch release.  To
this end, add a job like this:
Ralf Jung's avatar
Ralf Jung committed
94

Ralf Jung's avatar
Ralf Jung committed
95
96
97
98
```
build-iris.dev:
  <<: *template
  variables:
99
100
101
    STDPP_REPO: "iris/stdpp"
    IRIS_REPO: "iris/iris"
    OPAM_PINS: "coq version 8.13.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
Ralf Jung's avatar
Ralf Jung committed
102
103
104
105
  except:
  only:
  - triggers
  - schedules
Ralf Jung's avatar
Ralf Jung committed
106
  - api
Ralf Jung's avatar
Ralf Jung committed
107
```
Ralf Jung's avatar
Ralf Jung committed
108

Ralf Jung's avatar
Ralf Jung committed
109
110
111
The last four lines configure this job to *not* run when new commits are pushed
to the repo, and instead make it run when a pipeline is triggered through the
REST API or by a schedule.  The pins are set up to install a development version
Ralf Jung's avatar
Ralf Jung committed
112
of all the dependencies, and the `8.10` branch of Coq.
Ralf Jung's avatar
Ralf Jung committed
113

114
The `STDPP_REV` and `IRIS_REV` variables can be set via an API request to test
115
116
117
this repository against different branches of std++ or Iris; `STDPP_REPO` and
`IRIS_REPO` can be set to fetch those branches from forks (see the `build-all`
script in the Iris repository.)
118
119

Now ask an admin to set up a pipeline schedule.  We usually only
Ralf Jung's avatar
Ralf Jung committed
120
121
do nightly builds for projects in the iris group; those schedules should be
"owned" by the `iris-dev` user so that the Iris development team gets the emails
122
123
about broken builds.  This can be achieved by having an admin follow these steps:
* At <https://gitlab.mpi-sws.org/admin/users/iris-dev>, click "Impersonate".
Ralf Jung's avatar
Ralf Jung committed
124
125
126
* Go to the schedule settings for the project you are setting up, and add the
  schedule. It will be owned by `iris-dev`. If you already created the schedule,
  you can "Take ownership" to make `iris-dev` own it.
127
* Click the button in the top-right corner to stop impersonating `iris-dev`.
Ralf Jung's avatar
Ralf Jung committed
128
129
130
131

## Timing

To track performance of the project, one of the jobs should look like this:
Ralf Jung's avatar
Ralf Jung committed
132

Ralf Jung's avatar
Ralf Jung committed
133
```
Ralf Jung's avatar
Ralf Jung committed
134
build-coq.8.10.0:
Ralf Jung's avatar
Ralf Jung committed
135
136
  <<: *template
  variables:
Ralf Jung's avatar
Ralf Jung committed
137
    OPAM_PINS: "coq version 8.10.0"
Ralf Jung's avatar
Ralf Jung committed
138
  tags:
Ralf Jung's avatar
Ralf Jung committed
139
140
141
  - fp-timing
```

142
143
144
145
146
The last two lines makes this job run on the more isolated runner.  This
automatically triggers measuring the performance of building every single file
of this project.  This information is submitted to the [coq-speed] server where
you can browse it in a web UI.  The "configuration" is set to the job name
(i.e., `build-coq.8.10.0` in the example above).
Ralf Jung's avatar
Ralf Jung committed
147
148
149
150
151

This requires setting the `TIMING_SECRET` CI variable.  Talk to an admin about
this.  The variable should *not* be protected because we do timing measurements
on all branches, not just `master`!

Ralf Jung's avatar
Ralf Jung committed
152
153
154
You also need to enable the `coop-timing` runner for your project. Again this
needs to be done by an admit.

Ralf Jung's avatar
Ralf Jung committed
155
156
157
158
Behind the scenes, the data is sent to our
[custom webhook](https://gitlab.mpi-sws.org/janno/gitlab-ci-webhook), which runs
on `coq-speed.mpi-sws.org` and locally stores the data in a PostgreSQL database.

Ralf Jung's avatar
Ralf Jung committed
159
[coq-speed]: https://coq-speed.mpi-sws.org/
Ralf Jung's avatar
Ralf Jung committed
160

Ralf Jung's avatar
Ralf Jung committed
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
### Ad-hoc timing

By "ad-hoc timing", we mean testing the performance effects of an Iris branch against downstream developments:
we do an "ad-hoc" timing run of the downstream development against both Iris master and the branch, and then we show a diff of those to runs.

To support this, the downstream project should already support nightly builds.
Furthermore, it needs to have an "ad-hoc timing job" that can be triggered like the nightly builds:

```

trigger-iris.timing:
  <<: *template
  variables:
    OPAM_PINS: "coq version 8.13.2   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
  tags:
  - fp-timing
  only:
  - triggers
  - schedules
  - api
  except:
    variables:
    - $TIMING_AD_HOC_ID == null
```

Furthermore, the nightly build needs to be disabled for these ad-hoc jobs by changing the `only` clause of `trigger-iris.dev` to

```
  only:
    refs:
    - triggers
    - schedules
    - api
    variables:
    - $TIMING_AD_HOC_ID == null
```

Basically, this means that when a pipeline is triggered without the `TIMING_AD_HOC_ID` variable being set, it continues to treat this like a nightly build.
When the pipeline variable `TIMING_AD_HOC_ID` is set, it instead does an ad-hoc timing run.
The `buildjob` script in this repository will take care of submitting this timing information to the `coq-speed.mpi-sws.org` server with the right metadata.

The best way to trigger these ad-hoc timing builds is via the `iris-bot` script in the Iris repository.

Ralf Jung's avatar
Ralf Jung committed
204
205
206
## Opam publishing

Those of our projects that have reverse dependencies get automatically published
Ralf Jung's avatar
Ralf Jung committed
207
on [our opam repo][opam].  Set the `OPAM_PKG` variable to the name of the
Ralf Jung's avatar
Ralf Jung committed
208
package to make that happen.  This requires a per-project secret, see
Ralf Jung's avatar
Ralf Jung committed
209
210
[the private opam-updater documentation][opam-updater] for more details.  Be
careful to only set `OPAM_PKG` in one job, or your builds will fail because the
211
212
213
214
215
same commit gets published several times.

To avoid the secret from leaking without any trace, absolutely make sure that
you have set up branch protection for the wildcard pattern `master*` in the
repository configuration!
Ralf Jung's avatar
Ralf Jung committed
216
217
218

[opam]: https://gitlab.mpi-sws.org/iris/opam
[opam-updater]: https://gitlab.mpi-sws.org/iris/opam-updater
Ralf Jung's avatar
Ralf Jung committed
219
220
221
222
223
224
225
226
227
228
229

## coqdoc publishing

We can automatically deploy the generated coqdoc for a project to
[the web][coqdoc].  To make this happens, set `DOC_DIR` to an rsync path where
the docs should be pushed to; usually that's something like
`"coqdoc@center.mpi-sws.org:projectname"`.  You also need to add the secret part
of an SSH key that can access this location in the `DOC_KEY` variable (that
should be a protected variable because it is only needed by the `master`
branch).  Preferably, use a fresh key for each project.  For
`coqdoc@center.mpi-sws.org`, these keys should be set up as follows in
Ralf Jung's avatar
Ralf Jung committed
230
`~/.ssh/authorized_keys`:
Ralf Jung's avatar
Ralf Jung committed
231
232
233
234
235
236
237
238

```
command="$HOME/rrsync /www/sws-websites/plv.mpi-sws.org/coqdoc/",no-port-forwarding,no-X11-forwarding,no-agent-forwarding,no-pty
```

This restricts the key to only be able to run rsync for this particular
directory.

239
240
241
242
To avoid the secret from leaking without any trace, absolutely make sure that
you have set up branch protection for the wildcard pattern `master*` in the
repository configuration!

Ralf Jung's avatar
Ralf Jung committed
243
[coqdoc]: https://plv.mpi-sws.org/coqdoc
Ralf Jung's avatar
Ralf Jung committed
244
245
246
247
248

## Backend

Some information about the servers that make this all work can
[be found here](srvr-doc.md).