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

src/Lean/Compiler/LCNF/EmitC.lean

@@ -1077,35 +1077,40 @@ where
       "#if defined(WIN32) || defined(_WIN32)",
       "#include <windows.h>",
       "#endif",
+      "lean_object* run_main(int argc, char ** argv) {"
+    ]
+    if ps.size == 2 then
+      emitLns [
+        "    lean_object* in = lean_box(0);",
+        "    int i = argc;",
+        "    while (i > 1) {",
+        "      lean_object* n;",
+        "      i--;",
+        "      n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);",
+        "      in = n;",
+        "    }"
+      ]
+      emitLn <| "    return " ++ leanMainFn ++ "(in);"
+    else
+      emitLn <| "    return " ++ leanMainFn ++ "();"
+    emitLns [
+      "}",
       "int main(int argc, char ** argv) {",
       "#if defined(WIN32) || defined(_WIN32)",
       "  SetErrorMode(SEM_FAILCRITICALERRORS);",
       "  SetConsoleOutputCP(CP_UTF8);",
       "#endif",
-      "  lean_object* in; lean_object* res;",
+      "  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);",
+      "  }"
     ]
-    if ps.size == 2 then
-      emitLns [
-        "    in = lean_box(0);",
-        "    int i = argc;",
-        "    while (i > 1) {",
-        "      lean_object* n;",
-        "      i--;",
-        "      n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);",
-        "      in = n;",
-        "    }"
-      ]
-      emitLn <| "    res = " ++ leanMainFn ++ "(in);"
-    else
-      emitLn <| "    res = " ++ leanMainFn ++ "();"
-    emitLn "  }"
     -- `IO _`
     let retTy := env.find? `main |>.get! |>.type |>.getForallBody
     -- either `UInt32` or `(P)Unit`

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
 
 /--

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

src/library/ir_interpreter.cpp

@@ -1177,8 +1177,8 @@ uint32 run_main(elab_environment const & env, options const & opts, list_ref<str
     return interpreter::with_interpreter<uint32>(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<string_ref>, args));
     return ret;
 }

src/runtime/thread.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include <vector>
 #include <iostream>
+#include <cstring>
 #ifdef LEAN_WINDOWS
 #include <windows.h>
 #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<void()>(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() {