!bench against commit?

Stream: mathlib4

[Thomas Murrills]

This might have a simple answer: is there syntax to bench against a specific commit (possibly in a different branch)? Specifically, I want to bench a test of a lean4 PR against nightly-testing.

If not I suppose I’ll have to make a PR and bench it, then compare in the speedcenter, then close the PR. But if it doesn’t exist already, !bench against (<branch>?):<commit> might be a useful feature to have. :) (Also note that running things locally is not really feasible on my machine.)

[Matthew Ballard]

There is a comparison feature where you can choose two commits and get a perf diff.

[Thomas Murrills]

In the speedcenter, right? Doesn’t that mean I need to open 2 PRs?

[Matthew Ballard]

In the speedcenter web interface yes. You will need to get runs for both of them so you'll need two PRs (modulo unusual provenance).

[Thomas Murrills]

Right, I know I can do that, my question is specifically about a command like !bench against … on a single mathlib PR. :)

[Matthew Ballard]

No such command exists. The general assumption is that you are benching off the commit you branched from master.

[Thomas Murrills]

Ah, okay. In that case I’d like to turn this thread into a feature request, since there are a few scenarios in which we don’t want to bench against that commit. :)

[Joachim Breitner]

I had the same desire. My work around was to create a temporary PR with that commit at tbre head, run !bench, and delete the PR again. (For me it would suffice to have !bench abcdef, I can then click that comparison in the web view manually)

[Matthew Ballard]

With the PR, you have CI run on the commit which is prophylactic for empty benchmarking runs.

[Thomas Murrills]

CI runs on branches without PRs anyway, no?

[Joachim Breitner]

A small QoL improvement would be if !bench would schedule not just the HEAD commit of the branch, but also the base commit (the merge-base), which is usually what you would want to compare against (assuming that scheduling a commit is idempotent).

[Sebastian Ullrich]

Java contributions welcome! :) https://github.com/IPDSnelting/velcom

[Joachim Breitner]

The code changes to might actually be doable by cargo-culting existing Java code, if the Github API would include more sensible data, but (again) it doesn’t, and one would have to run git merge-base manually… so nevermind.

[Sebastian Ullrich]

Velcom has to have the information eventually in order to generate the diff I suppose, but what you're saying is that it doesn't have it at this specific place?

[Joscha Mennicken]

Velcom finds the base commit for comparisons here using this fancy recursive query that traverses the PR until it finds one or more tracked commits. A tracked commit is a commit reachable from a tracked branch (in lean's and mathlib's case, that's only master). For example, in this commit graph

A - B - C - D - E (master)
     \       \
      F - G - H - I (pr)

commits A, B, C, D, and E are tracked and getFirstParentsOfBranch will return B and D.

[Joachim Breitner]

Not within three lines of looking up and down :-)

[Joachim Breitner]

So one could use this logic to find a good compareToHash before scheduling the actual !bench PR head, check if it had been run before, and if not, schedule it. So later replyToFinishedPrCommands would (more likely) find a run to compare against. Not sure how frequent that need is to add that logic, it might be easier to support !bench <commit> or hand out access to the UI to those who are bothered.

[Joscha Mennicken]

!bench <commit> would need similar logic to schedule <commit> (checking whether a run exists and if not, adding one to the queue)