From 609a05a90a7c25cb55ee4399eb678b2679fd1ffa Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 20 Mar 2026 16:40:00 +0100 Subject: [PATCH] feat: increase default stack size from 8MB to 1GB (#12971) 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. --- src/Lean/Compiler/LCNF/EmitC.lean | 39 +++++++++++++++++-------------- src/Lean/Shell.lean | 2 +- src/include/lean/lean.h | 2 ++ src/library/ir_interpreter.cpp | 4 ++-- src/runtime/thread.cpp | 35 +++++++++++++++++++++++++-- 5 files changed, 60 insertions(+), 22 deletions(-) diff --git a/src/Lean/Compiler/LCNF/EmitC.lean b/src/Lean/Compiler/LCNF/EmitC.lean index d88eb484b4..ae5728c8f7 100644 --- a/src/Lean/Compiler/LCNF/EmitC.lean +++ b/src/Lean/Compiler/LCNF/EmitC.lean @@ -1077,23 +1077,11 @@ where "#if defined(WIN32) || defined(_WIN32)", "#include ", "#endif", - "int main(int argc, char ** argv) {", - "#if defined(WIN32) || defined(_WIN32)", - " SetErrorMode(SEM_FAILCRITICALERRORS);", - " SetConsoleOutputCP(CP_UTF8);", - "#endif", - " lean_object* in; lean_object* res;", - " argv = lean_setup_args(argc, argv);", - if usesLeanAPI then " lean_initialize();" else " lean_initialize_runtime_module();", - s!" res = {← getModInitFn (phases := if env.header.isModule then .runtime else .all)}(1 /* builtin */);", - " lean_io_mark_end_initialization();", - " if (lean_io_result_is_ok(res)) {", - " lean_dec_ref(res);", - " lean_init_task_manager();", + "lean_object* run_main(int argc, char ** argv) {" ] if ps.size == 2 then emitLns [ - " in = lean_box(0);", + " lean_object* in = lean_box(0);", " int i = argc;", " while (i > 1) {", " lean_object* n;", @@ -1102,10 +1090,27 @@ where " in = n;", " }" ] - emitLn <| " res = " ++ leanMainFn ++ "(in);" + emitLn <| " return " ++ leanMainFn ++ "(in);" else - emitLn <| " res = " ++ leanMainFn ++ "();" - emitLn " }" + emitLn <| " return " ++ leanMainFn ++ "();" + emitLns [ + "}", + "int main(int argc, char ** argv) {", + "#if defined(WIN32) || defined(_WIN32)", + " SetErrorMode(SEM_FAILCRITICALERRORS);", + " SetConsoleOutputCP(CP_UTF8);", + "#endif", + " lean_object* res;", + " argv = lean_setup_args(argc, argv);", + if usesLeanAPI then " lean_initialize();" else " lean_initialize_runtime_module();", + s!" res = {← getModInitFn (phases := if env.header.isModule then .runtime else .all)}(1 /* builtin */);", + " lean_io_mark_end_initialization();", + " if (lean_io_result_is_ok(res)) {", + " lean_dec_ref(res);", + " lean_init_task_manager();", + " res = lean_run_main(&run_main, argc, argv);", + " }" + ] -- `IO _` let retTy := env.find? `main |>.get! |>.type |>.getForallBody -- either `UInt32` or `(P)Unit` diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean index 6e45280a21..2ff5c4b0c8 100644 --- a/src/Lean/Shell.lean +++ b/src/Lean/Shell.lean @@ -31,7 +31,7 @@ abort on files with invalid UTF-8. opaque decodeLossyUTF8 (a : @& ByteArray) : String /- Runs the `main` function of the module with `args` using the Lean interpreter. -/ -@[extern "lean_run_main"] +@[extern "lean_eval_main"] opaque runMain (env : @& Environment) (opts : @& Options) (args : @& List String) : BaseIO UInt32 /-- diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 015cf3b38d..159f977c3c 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -3245,6 +3245,8 @@ static inline double lean_float_once(double* loc, lean_once_cell_t* tok, double return lean_float_once_cold(loc, tok, init); } +LEAN_EXPORT lean_object * lean_run_main(lean_object * (*main_fn)(int, char **), int argc, char ** argv); + #ifdef __cplusplus } #endif diff --git a/src/library/ir_interpreter.cpp b/src/library/ir_interpreter.cpp index a356cf342b..70cdb1453f 100644 --- a/src/library/ir_interpreter.cpp +++ b/src/library/ir_interpreter.cpp @@ -1177,8 +1177,8 @@ uint32 run_main(elab_environment const & env, options const & opts, list_ref(env, opts, "main", [&](interpreter & interp) { return interp.run_main(args); }); } -/* runMain (env : Environment) (opts : Iptions) (args : List String) : BaseIO UInt32 */ -extern "C" LEAN_EXPORT uint32_t lean_run_main(b_obj_arg env, b_obj_arg opts, b_obj_arg args) { +/* runMain (env : Environment) (opts : Options) (args : List String) : BaseIO UInt32 */ +extern "C" LEAN_EXPORT uint32_t lean_eval_main(b_obj_arg env, b_obj_arg opts, b_obj_arg args) { uint32 ret = run_main(TO_REF(elab_environment, env), TO_REF(options, opts), TO_REF(list_ref, args)); return ret; } diff --git a/src/runtime/thread.cpp b/src/runtime/thread.cpp index ba06b37d13..d0d67f5f8f 100644 --- a/src/runtime/thread.cpp +++ b/src/runtime/thread.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include #include +#include #ifdef LEAN_WINDOWS #include #else @@ -20,7 +21,11 @@ Author: Leonardo de Moura #include "runtime/stack_overflow.h" #ifndef LEAN_DEFAULT_THREAD_STACK_SIZE -#define LEAN_DEFAULT_THREAD_STACK_SIZE 8*1024*1024 // 8Mb +#ifdef LEAN_EMSCRIPTEN +#define LEAN_DEFAULT_THREAD_STACK_SIZE 8*1024*1024 // 8MB for 32-bit +#else +#define LEAN_DEFAULT_THREAD_STACK_SIZE 1024*1024*1024 // 1GB for 64-bit +#endif #endif namespace lean { @@ -96,8 +101,10 @@ struct lthread::imp { imp(runnable const & p) { runnable * f = new std::function(mk_thread_proc(p, get_max_heartbeat())); + // Without `IS_A_RESERVATION`, `m_thread_stack_size` would be the initial *commit* size, + // quickly exhausting the available address space with our large default stack size. m_thread = CreateThread(nullptr, m_thread_stack_size, - _main, f, 0, nullptr); + _main, f, STACK_SIZE_PARAM_IS_A_RESERVATION, nullptr); if (m_thread == NULL) { throw exception("failed to create thread"); } @@ -163,6 +170,30 @@ extern "C" LEAN_EXPORT lean_obj_res lean_internal_set_thread_stack_size(size_t s return lean_box(0); } +extern "C" LEAN_EXPORT lean_object * lean_run_main(lean_object * (*main_fn)(int, char **), int argc, char ** argv) { +#ifdef LEAN_MULTI_THREAD + const char * stack_size_env = std::getenv("LEAN_STACK_SIZE_KB"); + if (stack_size_env) { + size_t sz = std::strtoull(stack_size_env, nullptr, 10); + sz = sz / 4 * 4 * 1024; // as in `Shell` + if (sz > 0) { + lthread::set_thread_stack_size(sz); + } + } + const char * use_thread_env = std::getenv("LEAN_MAIN_USE_THREAD"); + if (use_thread_env && std::strcmp(use_thread_env, "0") == 0) { + return main_fn(argc, argv); + } + // Start new thread to use given/default stack size + lean_object * res = nullptr; + lthread t([&]() { res = main_fn(argc, argv); }); + t.join(); + return res; +#else + return main_fn(argc, argv); +#endif +} + LEAN_THREAD_VALUE(bool, g_finalizing, false); bool in_thread_finalization() {