feat: increase default stack size from 8MB to 1GB

[Kha]

This PR increases Lean's default stack size, including for the main thread of Lean executables, to 1GB.

As stack pages are allocated dynamically, this should not change the memory usage of programs but can prevent them from stack overflowing.

The stack size (of any Lean thread) can now be customized via the LEAN_STACK_SIZE_KB environment variable. main can be prevented from running on a new thread by setting LEAN_MAIN_USE_THREAD=0, in which case the default OS stack size management applies to the main thread again.

[Kha]

!bench

[leanprover-radar]

Benchmark results for 938bb81 against 61a3443 are in. Significant changes detected! @Kha

• 🟥 build//instructions: +4.6G (+0.04%)

Large changes (5🟥)

• 🟥 compiled/liasolver//instructions: +232.5M (+5.63%)
• 🟥 compiled/nat_repr//instructions: +674.7M (+20.85%)
• 🟥 compiled/qsort//instructions: +1.9G (+11.24%)
• 🟥 compiled/unionfind//instructions: +4.3G (+17.25%)
• 🟥 compiled/workspaceSymbolsNewRanges//instructions: +30.5M (+4.11%)

Medium changes (1✅, 2🟥)

• 🟥 compiled/binarytrees.st//instructions: +45.9M (+0.07%)
• ✅ compiled/const_fold//instructions: -229.8M (-2.61%)
• 🟥 compiled/iterators//instructions: +6.1M (+1.07%)

Small changes (2✅, 4🟥)

• ✅ compiled/hashmap//instructions: -2.1M (-0.06%)
• 🟥 compiled/qsort//task-clock: +66ms (+5.90%)
• 🟥 compiled/qsort//wall-clock: +66ms (+5.88%)
• ✅ compiled/treemap//instructions: -2.5M (-0.01%)
• 🟥 lake/inundation/config import//task-clock: +8ms (+5.36%)
• 🟥 lake/inundation/config import//wall-clock: +8ms (+5.42%)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-18 21:36:17)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12971 has successfully built against this PR. (2026-03-18 22:30:08) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12971 has successfully built against this PR. (2026-03-19 13:15:36) View Log

[Kha]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@0458de3 against leanprover-community/mathlib4-nightly-testing@a0c49ce are in. Significant changes detected! @Kha

• 🟥 build//instructions: +6.0G (+0.00%)

Large changes (1✅)

• ✅ build/profile/C code generation//wall-clock: -161ms (-1.41%)

Small changes (2✅, 2🟥)

• 🟥 build/module/Mathlib.RingTheory.Polynomial.ShiftedLegendre//instructions: +1.3G (+10.64%)
• 🟥 build/module/Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence//instructions: +595.1M (+3.28%)
• ✅ build/profile/import//wall-clock: -1m 28s (-1.36%)
• ✅ build/profile/interpretation//wall-clock: -2m 47s (-1.78%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12971 has successfully built against this PR. (2026-03-20 13:17:32) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12971 has successfully built against this PR. (2026-03-20 14:31:43) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12971 has successfully built against this PR. (2026-03-20 16:50:30) View Log