Zulip Chat Archive

Stream: lean4

Topic: Running bench on CI?


Siddharth Bhat (Oct 15 2021 at 11:23):

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 (Oct 15 2021 at 11:24):

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.


Last updated: Dec 20 2023 at 11:08 UTC