search

coq / coq-bench

Scripts for differential performance testing of Coq packages / versions
Other
4 stars 6 forks source link

Fix #90 (re-enable autobenchmarking) #91

Closed JasonGross closed 3 years ago

JasonGross commented 4 years ago

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 commented 4 years ago

Why is bignums failing to install?

INFO: failed to install coq-bignums
ejgallego commented 4 years ago

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 commented 4 years ago

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

ejgallego commented 4 years ago

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 commented 4 years ago

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

JasonGross commented 4 years ago

@ejgallego Any update on this?

ejgallego commented 4 years ago

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

ejgallego commented 4 years ago

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

JasonGross commented 4 years ago

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

ejgallego commented 4 years ago

@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 commented 4 years ago

@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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

trigger benchmarking just by adding the needs:benchmarking label

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

JasonGross commented 4 years ago

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

ejgallego commented 3 years ago

Not relevant after the migration IIANM.