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

[Robin Arnez]

The message data is not constructed very effectively, try this:

import Lean.Meta.Basic

def Lean.MessageData.joinSepArray (a : Array MessageData) (sep : MessageData) : MessageData :=
  if h : a.size = 0 then ""
  else go 0 a.size (Nat.zero_lt_of_ne_zero h) (Nat.le_refl _)
where
  go (start : Nat) (stop : Nat) (h : start < stop) (h' : stop ≤ a.size) : MessageData :=
    let mid := (start + stop) / 2
    if h : mid = start then
      a[start]
    else
      let left := go start mid (by omega) (by omega)
      let right := go mid stop (by omega) (by omega)
      left ++ sep ++ right

run_meta do
  let n := 131096
  let c := Lean.MessageData.joinSepArray (Array.replicate n "a") ", "
  --Lean.logInfo c

I found that after uncommenting the line and then going onto run_meta it takes just a short while and then it crashes with "window not responding"

[Robin Arnez]

However, constructing the message data is pretty fast

[Robin Arnez]

Screenshot 2025-05-02 152343.png