coq/bot

@coqbot bench should allow customizing the list of packages to bench

Opened this issue · 4 comments

JasonGross commented

See coq/coq#15860 (comment) 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.

Alizter commented

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.

SkySkimmer commented

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

  • 👀1
Alizter commented

OK I did not know that, good to know. Then we can probably do this quite easily.

SkySkimmer commented

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)

  • 😄1