Increase stack space (for Aesop)

Stream: lean4

[Asta Halkjær From]

I am toying with Aesop, hoping it will find a proof term for me if I let it run long enough.
Unfortunately, simply beefing up Aesop's maxRuleApplications isn't enough as I then run into:

maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

And when I increase that, I run into:

libc++abi: terminating with uncaught exception of type lean::throwable: deep recursion was detected at 'interpreter' (potential solution: increase stack space in your system)

Can I increase the stack space somehow?

[Henrik Böving]

On linux you would use ulimit, specifically ulimit -s $SIZE to increase the system stack space as suggestion by the exception.

[Asta Halkjær From]

Thanks. How does this work with running Lean inside vscode?

[Sebastian Ullrich]

Using the new precompileSubmodules package option in Aesop's lakefile.lean should also fix this, and speed up Aesop quite a bit as documented in the other thread /cc @Jannis Limperg

[Jannis Limperg]

Has this precompile stuff landed yet? I can't find it in today's nightly. I'll take it as soon as possible of course!

[Sebastian Ullrich]

Yes, it should be https://github.com/leanprover/lake/releases/tag/v3.2.0

[Calvin Lee]

Asta Halkjær From said:

Can I increase the stack space somehow?

Way back when i used to build lean with leanmake LEANC_OPTS="-fsplit-stack -O3 -DNDEBUG" bin which would use a special gcc option to give unlimited stack space using linked stacks.
im pretty sure you could do the same thing with leancArgs in lake

[Jannis Limperg]

I've now enabled precompileModules for Aesop. Thanks @Mac for fixing the remaining issues, and of course for implementing this amazing feature in the first place!

[Asta Halkjær From]

Great! Aesop is noticeably faster now and it takes way longer before I run out of stack space.