Profiling Lean code execution

Stream: general

[Samuel Chassot]

Hi everyone,

I would like to profile the execution of some lean code. I would like to get a profile of executing the code at runtime, not the proofs/tactics. I could not find anything for the current lean version, apart from profiling the generated C executable with usual profilers.

Is there a canonical lean profiler? Or should I profile the executable with usual techniques?

Thanks a lot :)

[Sebastian Ullrich]

The usual techniques work quite well, I use samply a lot on Lean code

[Samuel Chassot]

Sebastian Ullrich said:

The usual techniques work quite well, I use samply a lot on Lean code

Perfect, thanks! I'll try that :)