slow crutches

Stream: new members

[Julian Berman]

Sometimes running hint or suggest 3 in a proof is incredibly slow (and may even timeout but I never have patience to wait longer than 20 seconds or so). Is there something I can run to see what's slowing these down in cases like this? Is it that there are lots of declarations in the environment and they're getting lost looking through lots of things?

[Henrik Böving]

There is most likely some tracing set_option you can use although I don't know how far these facilities are developed in Lean 3