Commit 315695de authored by Ralf Jung's avatar Ralf Jung
Browse files

document ad-hoc timing

parent 22be7678
...@@ -158,6 +158,49 @@ on `coq-speed.mpi-sws.org` and locally stores the data in a PostgreSQL database. ...@@ -158,6 +158,49 @@ on `coq-speed.mpi-sws.org` and locally stores the data in a PostgreSQL database.
[coq-speed]: https://coq-speed.mpi-sws.org/ [coq-speed]: https://coq-speed.mpi-sws.org/
### 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.
## Opam publishing ## Opam publishing
Those of our projects that have reverse dependencies get automatically published Those of our projects that have reverse dependencies get automatically published
......
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