deterministic timeout

Stream: maths

[Ashvni Narayanan]

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

https://github.com/leanprover-community/mathlib/blob/a1cae262dbc9e32a113f15de0dffd155cadc0753/src/ring_theory/dedekind_domain.lean#L444

Any help is appreciated, thank you!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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!