fix: ensure lean_initialize is called when Lean is only privately imported (#14505)

This PR fixes a compiler issue where private imports of the `Lean`
library could lead to segfaults by ensuring the necessary call to
`lean_initialize` happens in each module's initializer when necessary.
As a follow-up clean up, the call to `lean_initialize_runtime_module` is
made implicit as well, meaning users of Lean as an FFI library do not
need to call these functions themselves anymore.

Author: Kha

src/Lean/Compiler/LCNF/EmitC.lean

@@ -1015,6 +1015,21 @@ def emitInitFn (phases : IRPhases) : EmitM Unit := do
     let fn := mkModuleInitializationFunctionName (phases := if phases == .all then .all else if imp.isMeta then .runtime else phases) imp.module pkg?
     emitLn s!"lean_object* {fn}(uint8_t builtin);"
     return some fn
+  -- Every module initializes the runtime for itself so that external users of a Lean library do
+  -- not have to. Modules using the `Lean` package call the full `lean_initialize` instead as
+  -- module visibility can hide such an import from downstream modules (including the final
+  -- executable's root); the `Lean` modules themselves are initialized by `lean_initialize` and so
+  -- must not call it themselves.
+  let modName ← getModName
+  let leanInitFn? :=
+    if phases == .comptime then
+      none
+    else if usesModuleFrom env `Lean && !(`Lean).isPrefixOf modName then
+      some "lean_initialize"
+    else
+      some "lean_initialize_runtime_module"
+  if let some fn := leanInitFn? then
+    emitLn s!"void {fn}();"
   let initialized := s!"_G_{mkModuleInitializationPrefix phases}initialized"
   emitLns [
     s!"static bool {initialized} = false;",
@@ -1023,6 +1038,8 @@ def emitInitFn (phases : IRPhases) : EmitM Unit := do
     s!"if ({initialized}) return lean_io_result_mk_ok(lean_box(0));",
     s!"{initialized} = true;"
   ]
+  if let some fn := leanInitFn? then
+    emitLn s!"{fn}();"
   impInitFns.forM fun fn => do
     withErrRet do
       emit s!"{fn}(builtin)"
@@ -1077,10 +1094,8 @@ where
     if ps.size != 1 && ps.size != 2 then
       throwError "invalid main function, incorrect arity when generating code"
     let env ← getEnv
-    let usesLeanAPI := usesModuleFrom env `Lean
     emitLns [
       "char ** lean_setup_args(int argc, char ** argv);",
-      if usesLeanAPI then "void lean_initialize();" else "void lean_initialize_runtime_module();",
       "#if defined(WIN32) || defined(_WIN32)",
       "#include <windows.h>",
       "#endif",
@@ -1109,7 +1124,6 @@ where
       "#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)) {",

src/initialize/init.cpp

@@ -20,10 +20,17 @@ extern "C" object* initialize_Init(uint8_t);
 extern "C" object* initialize_Std(uint8_t);
 extern "C" object* initialize_Lean(uint8_t);
 
+static bool g_initialized = false;
 /* Initializes the Lean runtime. Before executing any code which uses the Lean package,
 you must first call this function, and then `lean::io_mark_end_initialization`. In between
-these two calls, you may also have to run additional initializers for your own modules. */
+these two calls, you may also have to run additional initializers for your own modules.
+
+This function is, and needs to stay, idempotent; it is called by the generated initializer of every
+module using the Lean package, which may happen multiple times in a single executable. */
 extern "C" LEAN_EXPORT void lean_initialize() {
+    if (g_initialized)
+        return;
+    g_initialized = true;
     save_stack_info();
     initialize_util_module();
     uint8_t builtin = 1;

src/runtime/init_module.cpp

@@ -16,7 +16,13 @@ Author: Leonardo de Moura
 #include "runtime/libuv.h"
 
 namespace lean {
+// idempotent as it may be called both by the generated `main` and, via `lean_initialize`,
+// by generated module initializers
+static bool g_initialized = false;
 extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
+    if (g_initialized)
+        return;
+    g_initialized = true;
     initialize_alloc();
     initialize_debug();
     initialize_object();

tests/lake/examples/reverse-ffi/main.c

@@ -4,13 +4,10 @@
 extern uint64_t my_length(lean_obj_arg);
 
 // see https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=ffi-initialization
-extern void lean_initialize_runtime_module();
-extern void lean_initialize();
 extern void lean_io_mark_end_initialization();
 extern lean_object * initialize_rffi_RFFI(uint8_t builtin);
 
 int main() {
-  lean_initialize_runtime_module();
   lean_object * res;
   // use same default as for Lean executables
   uint8_t builtin = 1;

tests/pkg/exe_private_lean_import/.gitignore

@@ -0,0 +1 @@
+/.lake

tests/pkg/exe_private_lean_import/Foo.lean

@@ -0,0 +1,12 @@
+module
+
+import Lean.Environment
+
+/-!
+Uses the `Lean` package through a *private* `import`, so downstream modules do not see `Lean` in
+this module's public interface.
+-/
+
+public def checkEmptyEnv : IO Bool := do
+  let env ← Lean.mkEmptyEnvironment
+  return (env.find? `Nat).isNone

tests/pkg/exe_private_lean_import/Main.lean

@@ -0,0 +1,13 @@
+module
+
+import Foo
+
+/-!
+Regression test: this executable root does not visibly import `Lean` (it is only privately imported
+by `Foo`), but the linked binary still contains and initializes `Lean` code, so the generated code
+must fully initialize the Lean runtime (`lean_initialize`) before running `main`. Getting this
+wrong makes the executable crash at startup.
+-/
+
+public def main : IO Unit := do
+  IO.println s!"empty env has no Nat: {← checkEmptyEnv}"

tests/pkg/exe_private_lean_import/lakefile.toml

@@ -0,0 +1,9 @@
+name = "exe-private-lean-import"
+defaultTargets = ["main"]
+
+[[lean_lib]]
+name = "Foo"
+
+[[lean_exe]]
+name = "main"
+root = "Main"

tests/pkg/exe_private_lean_import/lean-toolchain

@@ -0,0 +1 @@
+../../../build/release/stage1

tests/pkg/exe_private_lean_import/run_test.sh

@@ -0,0 +1,7 @@
+rm -rf .lake
+lake build
+
+# Without full initialization of the Lean package (which is linked into the executable even though
+# it is not visibly imported into the root module), running the executable crashes.
+capture ./.lake/build/bin/main
+check_out_contains "empty env has no Nat: true"