Running bench on CI?

Stream: lean4

[Siddharth Bhat]

I have a change that seems to provide some performance improvement. On stdlib, it seems to provide a perf delta of speed up = 12.42%. Can I invoke !bench on the PR I created?? In general, if I sent a performance-related PR, can I invoke !bench on it?

I don't want to be a nuisance. But I'm not sure if I'm running the bench suite correctly, so having the CI run the bench for me would be super useful.

[Sebastian Ullrich]

You can't, the benchmarks are not sufficiently sandboxed that anyone should be able to run them :) . But I can definitely do it for you.