Commit 22be7678 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

Update srvr-doc.md

parent 546d2db0
......@@ -30,7 +30,7 @@ two servers are relevant
+ `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.
+ for creating/updating opam packages: https://gitlab.mpi-sws.org/iris/opam-updater (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.
......
Supports Markdown
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