diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index 8d8f445256..4ad3fc0318 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -187,7 +187,8 @@ def emitMainFn : M Unit := do let retTy := env.find? `main |>.get! |>.type |>.getForallBody -- either `UInt32` or `(P)Unit` let retTy := retTy.appArg! - emitLns ["if (lean_io_result_is_ok(res)) {", + emitLns ["lean_finalize_task_manager();", + "if (lean_io_result_is_ok(res)) {", " int ret = " ++ if retTy.constName? == some ``UInt32 then "lean_unbox_uint32(lean_io_result_get_value(res));" else "0;", " lean_dec_ref(res);", " return ret;", diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 603190da53..3739b88e46 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1063,6 +1063,7 @@ static inline lean_obj_res lean_thunk_get_own(b_lean_obj_arg t) { LEAN_SHARED void lean_init_task_manager(); LEAN_SHARED void lean_init_task_manager_using(unsigned num_workers); +LEAN_SHARED void lean_finalize_task_manager(); LEAN_SHARED lean_obj_res lean_task_spawn_core(lean_obj_arg c, unsigned prio, bool keep_alive); /* Run a closure `Unit -> A` as a `Task A` */ diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 992111706d..e2878c57a1 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -907,6 +907,13 @@ extern "C" LEAN_EXPORT void lean_init_task_manager() { lean_init_task_manager_using(hardware_concurrency()); } +extern "C" LEAN_EXPORT void lean_finalize_task_manager() { + if (g_task_manager) { + delete g_task_manager; + g_task_manager = nullptr; + } +} + scoped_task_manager::scoped_task_manager(unsigned num_workers) { lean_assert(g_task_manager == nullptr); #if defined(LEAN_MULTI_THREAD)