!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)

[Thomas Murrills]

Is the only way to bench the effect of a core PR on mathlib still to

1. make a mathlib4 PR for the lean-pr-testing branch
2. !bench that PR
3. make a mathlib4 branch that ends at the base of your lean-pr-testing branch
4. open a PR for that branch
5. run !bench on that PR as well
6. find both of these in the testing center?

If so, are there any plans to streamline this? (I'm considering trying to learn a bit of Java and/or SQL if necessary... :grinning_face_with_smiling_eyes:)

[Joachim Breitner]

That's still the status quo. Although I have since found that Velcom's API has an endpoint to schedule a git commit directly, but haven't put it in a script yet, and it needs a token. But it should be possible to build a little tool around this. (Step 6 would likely still be needed).