bench summaries

Stream: general

[Damiano Testa]

Inspired by @Michael Stoll's summaries of !bench outputs, I wrote an action that would automatically post a similar comment on every !bench result. You can see a version of this here.

[Damiano Testa]

Before I open a PR, I wanted to ask whether this would be desirable and feedback for different formats.

[Damiano Testa]

In particular, if you really want nested tables, it is possible, but would require injecting some html into the markdown. I would only look into this if there was some serious support for it! :smile:

[Joachim Breitner]

Not answering your question, but I sometimes have to compare bench results that are not the result of !bench, and would enjoy having a way to get a report likes yours from two git commit shas, or from a link like http://speed.lean-fro.org/mathlib4/compare/8c347d50-8923-404f-9e41-daa5fd4ab2f7/to/dfab2686-177b-44a1-afc4-b23a55bcce45

[Damiano Testa]

The action described above actually scrapes http://speed.lean-fro.org/mathlib4/compare/8c347d50-8923-404f-9e41-daa5fd4ab2f7/to/dfab2686-177b-44a1-afc4-b23a55bcce45, extracts the commit shas and then formats the json request to the speedcenter. Integrating this with what you want may be straightforward.

[Damiano Testa]

E.g., does this look like a reasonable summary for what you posted?

[Damiano Testa]

(I simply replaced your link into the analogous link from a different !bench and re-triggered the same action.)

[Kevin Buzzard]

I don't know much about CI, but I do know that I like very much Michael's summaries. But is there a chance that adding this will make our CI even more likely to fail/time out/whatever?

[Damiano Testa]

There is always the possibility of something breaking. However, this action is triggered on comments (not on push, so the regular build would be unaffected). I think that the worst that can happen is that the action fails and a message is not posted, not that the "core" mathlib CI will break.

[Damiano Testa]

In terms of speed, the "full" action takes about 20s, but this is only when the last message on the PR starts with Here are the [benchmark results], so most of the times, it will just take the time it takes it to realize that this is not the case and stop processing.

[Damiano Testa]

After all these reassurances, let me also admit that CI has ways of breaking that are always surprising and unexpected, so, the honest answer is: if this looks a good addition, then we should risk and see if it breaks anything substantial! :smile:

[Damiano Testa]

(In case it was not clear from my message above: the "regular" CI, the one that GitHub uses for the green tick and the one that bors uses for merging into master, is in a workflow file that is different from the file that encodes this new action, so the risk would be really minimal!)

[Damiano Testa]

#16488

[Damiano Testa]

You can see tests for this action and the script at the links above on Bryan's fork of mathlib.

[Jon Eugster]

https://github.com/leanprover-community/mathlib4/pull/16217#issuecomment-2381392953

both links of this !bench summary say "site cant be resched". Didnt look into it yet, does that have something to do with the new website?

[Sebastian Ullrich]

Works for me

[Jon Eugster]

Ah maybe the browser on my phone blocks it because its not a secure connection. Works on my laptop, too (where it should "connection not secure"). Sorry for the noise, must be a setting in my mobile browser.

[Damiano Testa]

I have never managed to view the benchmarks from my phone.

[Jon Eugster]

Ah, my phone sends me to https://speed.lean-fro.com instead of http://speed.lean-fro.com and the former cannot be reached. Probably the bot just needs to print the prefix http:// and it would work. Let me see if I find where that bot is located...

[Michael Rothgang]

I stumbled upon this PR and just left a review.

[Damiano Testa]

Bench summaries are now in mathlib!

If you bench your PR, after you receive the results, another bot should post a Michael-style summary as well.

[Damiano Testa]

This was just added, so let me know of any issues or missing posts!

Thanks!

[Michael Rothgang]

This report confused me for a moment: all metrics improve (i.e., go down) --- but the instructions show a negative percentage, while the percentage column shows a + sign. Can the percentage be fixed to match the other sign?

[Mauricio Collares]

The diff format was abandoned? That's a shame, I thought it was really clever.

[Damiano Testa]

Michael, I'll take a look: possibly I simply subtracted numbers in different orders for one report and for the other (or maybe it is just the formatting that needs to be aware of signs).

[Damiano Testa]

Mauricio, the comment on the PR does not supersede whatever output bench produces: it is just a summary, but you can still click on the bench output and view the complete report.

[Damiano Testa]

Damiano Testa said:

Michael, I'll take a look: possibly I simply subtracted numbers in different orders for one report and for the other (or maybe it is just the formatting that needs to be aware of signs).

It turns out that I changed the sign on purpose to be the wrong one: #18170 fixes the mistake.

[Damiano Testa]

And it's already merged: thanks Matt!

[Damiano Testa]

I am also happy that this is getting tested: I was worried that the speed-center troubles would delay using this tool.

[Joachim Breitner]

Joachim Breitner said:

Not answering your question, but I sometimes have to compare bench results that are not the result of !bench, and would enjoy having a way to get a report likes yours from two git commit shas, or from a link like http://speed.lean-fro.org/mathlib4/compare/8c347d50-8923-404f-9e41-daa5fd4ab2f7/to/dfab2686-177b-44a1-afc4-b23a55bcce45

Coming back to this – I see there is a bench_summary script in the mathlib repo, but it seems I that determining the URL to scrape and creating the report is rather tightly coupled. Have you thought about extracting the part that takes the two run ids and produces a markdown report from the rest? Even if just as a local function that I can invoke using run_cmd in VSCode would be helpful (but a command line tool/lake script maybe even more)

[Michael Rothgang]

IIRC from the PR's review discussion, the conclusion was that things could be refactored, but postponing that was fine until a use case came up. In other words, if you could use this functionality, I don't see why it can't be refactored :-)

[Joachim Breitner]

I see. I regularly look at urls like https://speed.lean-lang.org/mathlib4/compare/8c347d50-8923-404f-9e41-daa5fd4ab2f7/to/dfab2686-177b-44a1-afc4-b23a55bcce45 when working on Lean PRs, and would love to have an easy way to produce a report for that that I can paste.

[Damiano Testa]

My memory is that the speed-center identifies runs not by commit hash, but by something else that is hard to read "externally".

[Damiano Testa]

The only place where I know where to find it, is in the bot's message.

[Damiano Testa]

To be slightly more specific, comparing the github hashes

• git 77ffd776b7fb2a9fd4e4d96c32245eeed92e6924

and

• git fa9b36533f4059e2df709cff88edc6d9091cd4a6

in the speed-center, you should retrieve the "hashes"

• speed-center 988cf51c-aadd-4440-85ef-77a6d496aa6e

and

• speed-center d7a661e9-3f5f-47e2-8cd7-b465c89a18c3.

I got this information from this bot message, but I do not know how to get any direction of the correspondence git hash <--> speed-center hash, without relying on the bot message.

[Damiano Testa]

Reading your message now, if you already know the speed-center hashes, then extracting the markdown should be straightforward from the bench_summary script. Is this what you would like to have?

[Joachim Breitner]

Yes – although going from commit to run isn’t hard, this is the script that I am using:

~/build/lean $ cat speed-compare.sh
#!/usr/bin/env bash

rev1=$1
shift
rev2=$1
shift

if [ -z "$rev1" ] || [ -z "$rev2" ]
then
    echo "usage: $0 rev1 rev2"
fi

run1="$(curl -sS https://speed.lean-lang.org/mathlib4/api/commit/e7b27246-a3e6-496a-b552-ff4b45c7236e/$rev1 | jq -r '.commit.runs[0].id')"
run2="$(curl -sS https://speed.lean-lang.org/mathlib4/api/commit/e7b27246-a3e6-496a-b552-ff4b45c7236e/$rev2 | jq -r '.commit.runs[0].id')"
echo "https://speed.lean-lang.org/mathlib4/compare/$run1/to/$run2"

Pulling this into a bench report script would likely be reasonable.

[Damiano Testa]

Ok, so I think that your speed-compare script is the link that I was missing!

[Damiano Testa]

What would you like the command to do? Take as input two commit hashes and print the md report that the bench summary bot posts?

[Joachim Breitner]

Damiano Testa said:

What would you like the command to do? Take as input two commit hashes and print the md report that the bench summary bot posts?

Yes, that would be lovely. Maybe include a link to the comparison on speed.lean-lang.org (as I’d probably want that to be included always) and also the commits, to avoid confusion (guess a line containing links to these doesn't hurt on the PR notifications either, for posterity, so this hopefully needs no separate code path)