How to increase stack size in vscode

Stream: new members

[Isaac Li]

I'm working with Lean4 code in VSCode, and the Infoview gives me an error message: " ...(my file) crashed, likely due to a stack overflow or a bug. "Initially, I suspected a bug in my code. However, when I ran the same code using the Lean 4 Web editor, it executed without any issues. So I think the problem is about the stack size. Is there a way to increase the stack size for Lean 4?

[Derek Rhodes]

Hi, I couldn't find a reference to any relevant options having to do with memory limits or stack size in the Lean4Web repo, nor the vscode extension, however, digging around other places shows that people mentioning setting maxRecDepth directly in the editor with set_option. If that doesn't work, then maybe someone else knows :)

import Lean

# eval Lean.maxRecDepth  -- { name := `maxRecDepth, defValue := 512 }
set_option maxRecDepth 4096

(also, it might be worth considering that the behavior you're seeing may be the consequence of using a version of lean different from what's running on lean4web?)

#version -- Mathlib latest                 : Lean 4.18.0-rc1
#version -- Mathlib stable                 : Lean 4.17.0
#version -- Lean Nightly (without mathlib) : Lean 4.19.0-nightly-2025-03-24

[Sebastian Ullrich]

Can you reproduce the failure on the cmdline using lake lean? If so, try passing something like -- --tstack=16000 there.