## Stream: maths

### Topic: deterministic timeout

#### Ashvni Narayanan (Oct 29 2020 at 17:40):

I keep getting a (deterministic) timeout error, and can no longer see the status of the proof in the Lean infoview window.

Any help is appreciated, thank you!

#### Kevin Buzzard (Oct 29 2020 at 17:50):

Is this on a branch of mathlib? The link for some reason is not showing the branch name.

#### Kevin Buzzard (Oct 29 2020 at 17:52):

oh -- don't worry -- I can just checkout the commit and leanproject get-cache works anyway :D

#### Kevin Buzzard (Oct 29 2020 at 17:54):

I can't reproduce -- the file compiles fine for me (some sorries but no errors). Your proof is getting really long -- it might be worth trying to factor out some sublemmas?

#### Ashvni Narayanan (Oct 29 2020 at 18:13):

Kevin Buzzard said:

I can't reproduce -- the file compiles fine for me (some sorries but no errors). Your proof is getting really long -- it might be worth trying to factor out some sublemmas?

Yeah, I was going to do that at some point of time. Might as well do it now. Thank you!

Last updated: May 06 2021 at 18:20 UTC