Fix #90 (re-enable autobenchmarking)

[JasonGross]

Apparently variables left empty in the configuration don't get set at
all, rather than being set to the empty string. So we disable the
variable checks for variables allowed to be empty.

Fixes #90

[JasonGross]

Why is bignums failing to install?

INFO: failed to install coq-bignums

[ejgallego]

Why is bignums failing to install?

Likely the hash for the CI has to be bumped, that's a weakness of the current CI setup [PRs should update this hash]

[JasonGross]

Okay, bumped. Couldn't we use master and master^ for the commit "hashes", and thereby be more robust in the future?

[ejgallego]

Couldn't we use master and master^ for the commit "hashes", and thereby be more robust in the future?

Sure, if that works that would be great; I'm unsure what git can care from our variables tho.

[ejgallego]

I'm gonna push a bit more robust CI and then merge.

[JasonGross]

@ejgallego Any update on this?

[ejgallego]

I will take care of this ASAP, sorry for the delay.

[ejgallego]

With Jenkins offline I'm unsure what to do here :S

[JasonGross]

@maximedenes @ejgallego I'd be inclined to merge this, and propagate the changes to #12581, so the code does not bitrot. Thoughts?

[ejgallego]

@JasonGross I'm OK with any choice here, I'm afraid that I'm not up to date w.r.t. bench plans anymore so you'll have to sync with others.

[maximedenes]

@JasonGross now that we moved the bench infrastructure to Gitlab CI, is this still relevant?

Sorry for the confusion, we had to move quickly because we were notified of more security issues with Jenkins by the Inria IT services.

[JasonGross]

A lot of it is still relevant, yes. I think that it would still be nice for coqbot to automatically post the results of benchmarking to the PR, and it would be nice to be able to trigger benchmarking just by adding the needs:benchmarking label to the script. Should I prepare a version of this against coq/coq, now that the script lives there?

[maximedenes]

Should I prepare a version of this against coq/coq, now that the script lives there?

It would be nice yes, as the two features you mention certainly sound useful.

[JasonGross]

Actually, it looks like someone (@ppedrot?) already integrated all of this into the main Coq repo's bench script, so there's nothing to be done unless you want to sync the script in this repo with the one in coq/coq (in which case you should probably just merge this PR).

as the two features you mention certainly sound useful.

I think basically all that's left for these is the work on the coqbot side, as the script should already be sending post requests in any bench job where the coq_pr_number variable is set. (Well, I guess we also have to update the script to point at the right locations. I'll go prepare a PR to do that.)

[SkySkimmer]

trigger benchmarking just by adding the needs:benchmarking label

That's too agressive, the label can mean "after necessary fixups are done"

[JasonGross]

Perhaps it can trigger when someone comments @coqbot: benchmark?

[ejgallego]

Not relevant after the migration IIANM.