[#14505] fix: ensure lean_initialize is called when Lean is only privately imported

reference-manual/Manual/Runtime.lean

@@ -472,23 +472,18 @@ For modules in the Lean core (e.g., {module}`Init.Prelude`), the initializer is
 Module initializers will automatically initialize any imported modules.
 They are also idempotent (when run with the same `builtin` flag), but not thread-safe.
 
-*Important for process-related functionality*: applications that use process-related functions from `libuv`, such as {name}`Std.IO.Process.getProcessTitle` and {name}`Std.IO.Process.setProcessTitle`, must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) *before* calling `lean_initialize()` or `lean_initialize_runtime_module()`.
+*Important for process-related functionality*: applications that use process-related functions from `libuv`, such as {name}`Std.IO.Process.getProcessTitle` and {name}`Std.IO.Process.setProcessTitle`, must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) *before* calling any module initializer.
 This sets up process handling capabilities correctly, which is essential for certain system-level operations that Lean's runtime may depend on.
 
-Together with initialization of the Lean runtime, code like the following should be run exactly once before accessing any Lean declarations:
+Putting everything together, code like the following should be run exactly once before accessing any Lean declarations:
 ```C
-void lean_initialize_runtime_module();
-void lean_initialize();
 char ** lean_setup_args(int argc, char ** argv);
 
 lean_object * initialize_A_B(uint8_t builtin);
 lean_object * initialize_C(uint8_t builtin);
 ...
 
 argv = lean_setup_args(argc, argv); // if using process-related functionality
-lean_initialize_runtime_module();
-// necessary (and replaces `lean_initialize_runtime_module`) for code that (indirectly) accesses the `Lean` package:
-//lean_initialize();
 
 lean_object * res;
 // use same default as for Lean executables