determining where Lean is slow

Stream: general

[Jireh Loreaux]

Let's say you have a slow proof. How exactly do you go about figuring out where it is slow in order to speed it up? Obviously, you can use tricks like sorry; or commenting bits out, but surely there is a better way. What is it?

[Johan Commelin]

set_option profiler true is often helpful