Commit 546d2db0 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

Add new file

parent 2abf8eed
## Documentation for CI server config
two servers are relevant
- coop.mpi-sws.org
+ main CI machine, doesn't do anything else (CI-Jobs are running via docker)
+ accurate timings require some work wrt hardware & configs
+ two sockets (10cores each) to prevent interference when measuring timings
+ one socket for timing jobs, one socket for everything else
+ different sockets means different memory controllers, important for timings
+ config: `/etc/systemd/system.conf` sets cpu-affinity system (cpu topology can be validated with `lscpu`)
+ `/etc/gitlab-runner/config.toml` is the main config for the CI runner (affinity for timing jobs configured to avoid interference through SMT)
+ using S3-Server for caching (served by MPI)
+ for timing measurements: #instructions are measured with `perf` (less noisy than exact times)
+ server doesn't use custom kernel, but rather the standard Debian kernel (to enable `perf` in Docker)
+ sever is stateless, can be wiped anytime
- coq-speed.mpi-sws.org
+ runs in some VM somewhere, serves the `coq-speed.mpi-sws.org` frontend
+ PostreSQL + Grafana + home-made Rust-service to fill the DB with timing info (`https://gitlab.mpi-sws.org/iris/ci-timing-webhook`)
+ stateful, has a backup job
+ Grafana config:
- queries that put data in right format for Grafana, configured through the Grafana frontend
- hopefully won't have to touch those
+ CI scripts
- base-CI-image is on github.com/RalfJung/opam-ci (branch opam2)
- CI config (.gitlab-ci.yml) is identical for most projects
+ `tags` are used for setting the runner (`fp` (default), `fp-timing`)
+ `variables`: sets environment variables for CI, list with variables is at the top of https://gitlab.mpi-sws.org/iris/ci/-/blob/master/buildjob
+ `OPAM_PINS` variable: uses triples separated by spaces to configure opam pins (e.g. `coq-core.dev git git+https://....`); there's a shortcut for use with git repos containing `.opam` configs, just use `git+https://...` instead of the triple
+ `CI_RUNNER_DESCRIPTION`: parsed for activation of `perf`, sets the `TIMECMD` env variable (which is read by Coq); the `perf` script calls `perf` with the right parameters and concatenates the output files to one which is parsed by the frontend (this concatenated info is also shown in the CI output log on Gitlab)
+ ...
+ for creating/updating opam packages: `iris/opam-update` (private due to secrets) runs CI jobs for updating.
+ updating coqdocs: uses a `coqdoc` user which can only use rsync
+ `prepare-opam.sh`: uses a few opam workarounds; in case there are problems with the opam cache, use the `Clear Runner Caches` button on the pipeline overview in Gitlab. may need to clean up storage from time to time.
- iris: `iris-bot` script does two things: checking if reverse dependencies still build and checking two commits for timing differences. To do that, there are `trigger-iris.timing`/`trigger-iris.dev` CI jobs, CI is using the `TIMING_AD_HOC_ID` variable to check which one to run.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment