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.