Lean's stack size (58093 ought to be enough for anybody?)

Stream: new members

[Isak Colboubrani]

I’d like to increase Lean’s stack size—how can I do that, and how can I query the current setting?

For context, this is the test case that prompted me to look into the stack-size configuration:

% lean testcase_58093.lean | wc -l
   58093
% lean testcase_58094.lean | wc -l

Stack overflow detected. Aborting.
       0
zsh: abort      lean testcase_58094.lean |
zsh: done       wc -l
% cat testcase_58093.lean
import Lean.Meta.Basic
run_meta do
  let n := 58093
  let c := Lean.MessageData.ofList (List.replicate n "")
  Lean.log c
% cat testcase_58094.lean
import Lean.Meta.Basic
run_meta do
  let n := 58094
  let c := Lean.MessageData.ofList (List.replicate n "")
  Lean.log c

(I recognize there are code-level workarounds—such as iterating over the list—but for the sake of discussion, let’s assume the above code is immutable; I’m interested in how the stack size configuration works, and how it can be tweaked to make the second test case work as-is.)

[Isak Colboubrani]

I’m also curious whether the n=58093 limit here is specific to my setup, inherent to macOS (my OS) more broadly, or a universal default. Put differently, what’s the largest n your system can handle before triggering a stack overflow?

[Kyle Miller]

Stack size for programs is a general concept. You can query it on macOS on the command line like

% ulimit -s
8176

That's in kilobytes.

However, when Lean uses multithreading, there's configuration for the thread stack sizes.

% lean -h
...
  -s, --tstack=num       thread stack size in Kb
...

It looks like the default is either 8MB or 16MB, not sure.

I’m also curious whether the n=58093 limit here is specific to my setup

Yes, definitely. (Variables: which Lean version it is, how was the binary built, what ulimits you might have set, which versions of system libraries you have, and possible a couple other factors.)

[Kyle Miller]

Independently, there's also the maxRecDepth option inside Lean, which is intended to let Lean check that a recursion (likely) isn't going to overflow the stack. Increasing maxRecDepth doesn't increase the stack itself, so adjusting it should be done with care.

[Isak Colboubrani]

Thanks! When setting ulimit -s unlimited (which is ulimit -s 65520) I'm able to reach n=131096 (with a stack overflow at n=131097).

Is there some way to push n higher that does not require root access, or changing the code?

% ulimit -s unlimited
% ulimit -s
65520
% lean testcase_ulimit_max.lean | wc -l
  131096
% lean testcase_ulimit_max_succ.lean | wc -l

Stack overflow detected. Aborting.
       0
zsh: abort      lean testcase_ulimit_max_succ.lean |
zsh: done       wc -l
% cat testcase_ulimit_max.lean
import Lean.Meta.Basic
run_meta do
  let n := 131096
  let c := Lean.MessageData.ofList (List.replicate n "")
  Lean.log c
% cat testcase_ulimit_max_succ.lean
import Lean.Meta.Basic
run_meta do
  let n := 131096 + 1
  let c := Lean.MessageData.ofList (List.replicate n "")
  Lean.log c