coq
@coqbot bench should allow customizing the list of packages to bench
See https://github.com/coq/coq/pull/15860#issuecomment-1080460118 for motivation. I want to be able to write @coqbot bench coq-fiat-crypto-with-bedrock. Ideally coqbot would let me know immediately if any of the packages don't exist in the relevant opam setup, but this is not mandatory.
Currently bench jobs are set in dev/bench.sh and we selectively bench jobs by modifying that file temporarily. Coqbot probably shouldn't do this and we should have a better way to select jobs for the bench. I know that GitLab can have environment variables set on job start, so perhaps that is something we want to do.
We will therefore need to modify the bench set up in coq first before being able to do something like this.
Currently bench jobs are set in dev/bench.sh and we selectively bench jobs by modifying that file temporarily.
That's not how I do it, I just set the coq_opam_packages variable in the gitlab start job interface
OK I did not know that, good to know. Then we can probably do this quite easily.
Apparently it's only possible since this month ;) https://gitlab.com/gitlab-org/gitlab/-/issues/37267
Previously, when running a manual job it was only possible to specify variables through the UI, in this release we've added the ability to specify variables using REST API, which helps you speed up and automate your pipeline
(closed 2 weeks ago)