How to fix "(kernel) deep recursion detected"

Stream: new members

[Philogy]

I've noticed that as my proof has grown lean has become slower and slower. I seem to also be running into nonsensical bug/errors like (kernel) deep recursion detected.

What tips/tricks do you have in terms of structuring a proof that makes the IDE not slow down as much? Is it having fewer have lemmas in scope? Sectioning things off into top-level lemmas? I'm using the vim plugin, maybe the vscode version is more optimized?

Any tips for diagnosing / fixing the (kernel) deep recursion error would be appreciated.

[Philogy]

Also I'm encountering frequent crashes of the LSP. My file isn't that large ~300 lines so I assume I must be doing something wrong since other people seem to proving enormous things with it.

[Philogy]

My proof for anyone who's curious: https://gist.github.com/Philogy/127f5d0e6753b6c7ed304123deb0fc04

[Luigi Massacci]

I would hazard a guess that the gigantic numbers in the first couple lines are the source of your sorrows. Are you using compiler based tactics? Switching to those where possible might help, if you are carrying out a lot of computations

[Philogy]

Luigi Massacci said:

I would hazard a guess that the gigantic numbers in the first couple lines are the source of your sorrows. Are you using compiler based tactics? Switching to those where possible might help, if you are carrying out a lot of computations

Wdym by "compiler based tactics"?

I do some very limited computation with the numbers but it shouldn't cause any recursion, for instance computing Nat.xgcd (2^256) (2^256-1) which yields (1, -1) is simplified out at the beginning. It's only later when using the lemma on L226 does it trigger the deep recursion detected. Commenting that line out specifically resolves the deep recursion detected.

[Daniel Weber]

Splitting as much as you can to lemmas is a good idea, both for modularity and for faster elaboration.
Additionally, it might be good to define m0 and m1 using irreducible_def, as that prevents the kernel from reducing them, and proving what facts you need about them outside of the theorem, only substituting them there when you must. You can also try doing that for the other constants you have in the proof