Zulip Chat Archive

Stream: maths

Topic: deterministic timeout


view this post on Zulip 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.

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

Any help is appreciated, thank you!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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