Zulip Chat Archive
Stream: general
Topic: Timeout in a very large proof
Frédéric Dupuis (Jun 29 2022 at 23:59):
For the second time now, I'm getting a deterministic timeout in docs#vitali.exists_disjoint_covering_ae. This is a very large monolithic proof (~200 lines) that doesn't seem easy to break down into smaller lemmas and doesn't seem to have any particularly inefficient step either (at least the profiler doesn't reveal anything egregious, and the simps are already squeezed). Is there a way to increase the timeout on individual declarations that "deserve" it like this one?
Eric Wieser (Jun 30 2022 at 07:55):
I think you can use try_for 20000 { ... }
in the proof? I don't remember if that overrides the global timeout
Kevin Buzzard (Jun 30 2022 at 08:04):
You can always do the brutal extract_goal
in the middle and prove an aux
lemma. I did this in LTE once and it felt pretty dirty but it does the job
Frédéric Dupuis (Jun 30 2022 at 12:31):
Eric Wieser said:
I think you can use
try_for 20000 { ... }
in the proof? I don't remember if that overrides the global timeout
That does work, thanks!
Last updated: Dec 20 2023 at 11:08 UTC