!bench summary bug

Stream: mathlib4

[Damiano Testa]

I wrote the script to summarise the !bench output: I'll fix the issue, but won't get to it until much later today or, more likely, tomorrow.

[Damiano Testa]

It should be relatively straightforward, though, since if I remember correctly, all the formatting is done separately.

[Damiano Testa]

E.g., it should be just changing

https://github.com/leanprover-community/mathlib4/blob/master/scripts%2Fbench_summary.lean#L52

[Damiano Testa]

Are all percentages wrong by a factor of 10, or just the build ones?

[Daniel Weber]

If you import Mathlib.Data.String.Defs than you can add let decDigs := (toString decDigs).leftpad (c := '0') 2. However, this doesn't round to two digits, it floors instead. I think this kind of string formatting should be in batteries/core, not handled in this script

[Michael Rothgang]

(deleted)

[Damiano Testa]

I think that I identified the bug. The code discarded a "leading 0": it correctly computed the percentage to be 0. followed by 8 but printed 8 as a single digit number, instead of padding with 0 so that it was a 2-digit number that represented 8!

[Damiano Testa]

#18732

[Damiano Testa]

I also made the script a little more verbose, reporting command-line analogues of the commands that the lean script executes, since this might be useful for debugging and added some comments. Also, I took care of deprecations.

[Damiano Testa]

Let me know if you prefer to have a PR with just the fix and then a second one with these extra improvements.

[Notification Bot]

A message was moved here from #mathlib4 > typeclass inference in linarith by Heather Macbeth.

[Junyan Xu]

I've stopped seeing summaries in recent !bench calls.
Did the bot owner run out of quota or something?

[Damiano Testa]

I also noticed that, but did not get a chance to investigate.

[Junyan Xu]

Apparently the bot stopped even reacting to !bench now.

[Michael Rothgang]

#19733 was another instance.

[Michael Rothgang]

Benchmarking of merged PRs seems also missing.
@Sebastian Ullrich Is there anything suspicious going on with the benchmarking runner?

[Sebastian Ullrich]

I hit the server process with a wrench and restarted it. I also put a little robot next to it that hits it with the same wrench every 24 hours from now on.

[Michael Rothgang]

Reminds me of https://xkcd.com/538/ - hopefully not that kind of wrench :-)