Causal profiling

Stream: lean4

[James Gallicchio]

Would there be interest in a wrapper for Coz? Could be useful as we are working out the right way to test code :)

[James Gallicchio]

(And I could probably get a lake script working that automatically runs your code with coz and stuff)

[Leonardo de Moura]

I never used Coz, but it sounds interesting. I am a big fan of perf+hotspot. How do they compare to each other?

[James Gallicchio]

I'm not really familiar with any of the three, but Coz finds code segments that will improve the overall throughput/latency, which is NOT necessarily the code segments that the most time is spent on (which is moreso what I think perf tells you about?).

I believe Coz also does some additional work to ensure benchmarks aren't affected by things like code alignment, which can wildly affect code performance purely on the basis of how the C compiler arranges your code, not what your code is actually doing