benchmarking

Stream: CSLib

[Chris Henson]

@Joscha Mennicken I would like to set up benchmarking for leanprover/cslib. Is it possible for this repo to be included on https://radar.lean-lang.org/ and use the GitHub bot for !radar?

[Joscha Mennicken]

Yes, that should be possible. What kinds of benchmarks would you be interested in, and how much do you want to do yourself? I could give you an overview of the available options or just try to set up something similar to mathlib.

[Chris Henson]

I think similar to Mathlib is great if that is fairly straightforward to setup. A thread like #rss > Significant commits to mathlib4 would be nice. If there is anything you need on our end please let us know. Thank you!

[Fabrizio Montesi]

Yes, this would be great to have indeed! :blush:

[Joscha Mennicken]

https://radar.lean-lang.org/repos/cslib now exists, including GitHub and Zulip bots. For now, significance detection only considers build//instructions and doesn't look at the per-module instructions because the result was just too noisy. As I keep working on the mathlib4 significance detector, it should hopefully also improve for cslib.

For now, the benchmark suite lives in https://github.com/leanprover/radar-bench-cslib. If no issues pop up in the next few days, I plan on PR-ing it to the cslib repo. At that point, you should be able to add your own benchmarks or modify the existing ones without requiring my intervention. (Should you want to rename/reorganize benchmarks, I can rename the existing data so it matches the new names.)

If anything is broken or weird, or if you have any questions, please don't hesitate to let me know.

[Chris Henson]

Thank you for the quick turnaround! I've tested on a couple of PRs and it seems to be working.

[Joscha Mennicken]

CSLib had its first significant commit, confirming that the zulip bot works :D

[Joscha Mennicken]

We've switched to new runner hardware for everything except mathlib itself; you may see a jump in most metrics.

I've rebenchmarked the latest commit of main on the new hardware, so just make sure you've merged or rebased onto main before you use !bench/!radar.

[Joscha Mennicken]

I've switched cslib over to the same significance detection as mathlib uses (using historical data to set noise thresholds for noisy metrics).

I've also brought the benchmark suite itself more in line with the mathlib bench suite (though it's only a few small changes) and opened cslib#267.

[Chris Henson]

@Joscha Mennicken In Sebastian's Lean Together talk he mentioned radar reporting the critical build path. I see what appears to be some relevant code you added in your previous PR, but I do not see the same "Lakeprof report" links that Mathlib has for each commit. Is this something that could easily be added? I think it would be helpful for some performance profiling I'd like to do in the near future.

[Joscha Mennicken]

I've set up the lakeprof report in cslib#272, which should be ready to merge.

[Chris Henson]

Great, thank you!

[Chris Henson]

This confirms that System F makes up most of the critical path. (It's not listed here, but another area that needs work is LTS)

I will get to this eventually, but if anyone were interested in doing some initial work I think the place to start would be looking at the #grind_lint exceptions. Some of these may be solved using grind_pattern with constraints, I just haven't found the time to try this out yet.