relate to (deterministic) timeout

Stream: general

[Chenyi Li]

When I am coding the lean code, if I want to prove something very long, lean may tell me (deterministic) timeout. But if I cancel some part of the proof and replace it with the tactic "sorry", there is no problem with the code. So I may wonder how to deal with this problem, or how can I make the threshold time longer for lean?

[Martin Dvořák]

You can increase the threshold, but in the long term, it will probably create more pain.
I rather suggest avoiding compute-heavy tactics outside of the situations where they happen to work fast.

People will perhaps say that you should write shorter proofs (and have more lemmas).
I am not allowed to make this suggestions, as I sometimes write horribly long proofs.
Once I wrote a monolithic proof of 800 lines (please don't do what I did) and guess what -- I didn't get a timeout!

[Scott Morrison]

I am allowed to make this suggestion. :-) Proofs should be at most 10 lines. Show me a longer proof and I'll show you a missing lemma! (Not entirely true, but mostly.)

[Scott Morrison]

You can use set_option maxHeartbeats XXX in ... to raise the limit. But please please don't.

[Chenyi Li]

Thank you! And I will first increase the threshold, and I will then decompose my proof into shorter ones.

[Andrés Goens]

@Chenyi Li you might also find the save tactic useful if your proof takes quite a long time, you can insert a save in the middle of it and it won't recompute that part after you edit something underneath it