Zulip Chat Archive

Stream: general

Topic: deep recursion


view this post on Zulip Johan Commelin (Mar 12 2019 at 13:11):

How can I debug the following error?

deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

It showed up while trying to define a class. As far as I can see there is no loop or something...

view this post on Zulip Kenny Lau (Mar 12 2019 at 13:15):

have you tried turning Lean off and on again?

view this post on Zulip Johan Commelin (Mar 12 2019 at 13:15):

Yes, in fact I have.

view this post on Zulip Johan Commelin (Mar 12 2019 at 14:07):

I've found the culprit:

-- somewhere in the perfectoid project
local attribute [instance] topological_add_group.to_uniform_space

view this post on Zulip Johan Commelin (Mar 12 2019 at 14:18):

I've now put a section ... end around this attribute (and its one use) and the problem is gone.
So... this question is solved. Thanks for letting me rubber-duck this issue!


Last updated: May 08 2021 at 11:09 UTC