diff --git a/src/Lean/Compiler/LCNF/EmitC.lean b/src/Lean/Compiler/LCNF/EmitC.lean index d88eb484b410..ae5728c8f729 100644 --- a/src/Lean/Compiler/LCNF/EmitC.lean +++ b/src/Lean/Compiler/LCNF/EmitC.lean @@ -1077,12 +1077,30 @@ where "#if defined(WIN32) || defined(_WIN32)", "#include ", "#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 */);", @@ -1090,22 +1108,9 @@ where " 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` diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean index dd5c809b19d2..d99559f73541 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 015cf3b38d5b..159f977c3c7e 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 a356cf342b9f..70cdb1453fa8 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 ba06b37d1369..d0d67f5f8fcd 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() {