Timeout in a very large proof

Stream: general

[Frédéric Dupuis]

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]

I think you can use try_for 20000 { ... } in the proof? I don't remember if that overrides the global timeout

[Kevin Buzzard]

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]

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!