fix: mention libuv just because it's a low level api

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

doc/dev/ffi.md

@@ -131,14 +131,21 @@ Thus `[init]` functions are run iff their module is imported, regardless of whet
 
 The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules.
 Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe.
+
+**Important for process-related functionality**: If your application needs to use process-related functions from libuv, such as `Std.Internal.IO.Process.getProcessTitle` and `Std.Internal.IO.Process.setProcessTitle`, you 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()`. 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, you should execute code like the following 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 *);
 lean_object * initialize_C(uint8_t builtin, lean_object *);
 ...
 
+argv = lean_setup_args(argc, argv); // if using process-related functionality
 lean_initialize_runtime_module();
 //lean_initialize();  // necessary (and replaces `lean_initialize_runtime_module`) if you (indirectly) access the `Lean` package
 

src/Lean/Compiler/IR/EmitC.lean

@@ -143,6 +143,7 @@ def emitMainFn : M Unit := do
     unless xs.size == 2 || xs.size == 1 do throw "invalid main function, incorrect arity when generating code"
     let env ← getEnv
     let usesLeanAPI := usesModuleFrom env `Lean
+    emitLn "char ** lean_setup_args(int argc, char ** argv);";
     if usesLeanAPI then
        emitLn "void lean_initialize();"
     else
@@ -158,6 +159,7 @@ def emitMainFn : M Unit := do
   SetConsoleOutputCP(CP_UTF8);
   #endif
   lean_object* in; lean_object* res;";
+    emitLn "argv = lean_setup_args(argc, argv);";
     if usesLeanAPI then
       emitLn "lean_initialize();"
     else

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -1374,6 +1374,15 @@ def callLeanInitialize (builder : LLVM.Builder llvmctx) : M llvmctx Unit := do
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let _ ← LLVM.buildCall2 builder fnty fn #[]
 
+def callLeanSetupLibUV (builder : LLVM.Builder llvmctx) (argc argv : LLVM.Value llvmctx) : M llvmctx (LLVM.Value llvmctx) := do
+  let fnName := "lean_setup_args"
+  let intTy ← LLVM.i32Type llvmctx
+  let charPtrPtrTy ← LLVM.pointerType (← LLVM.pointerType (← LLVM.i8Type llvmctx))
+  let argtys := #[intTy, charPtrPtrTy]
+  let fnty ← LLVM.functionType charPtrPtrTy argtys
+  let fn ← getOrCreateFunctionPrototype (← getLLVMModule) intTy fnName argtys
+  LLVM.buildCall2 builder fnty fn #[argc, argv]
+
 def callLeanInitializeRuntimeModule (builder : LLVM.Builder llvmctx) : M llvmctx Unit := do
   let fnName :=  "lean_initialize_runtime_module"
   let retty ← LLVM.voidType llvmctx
@@ -1479,6 +1488,12 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
   let inslot ← buildPrologueAlloca builder (← LLVM.pointerType inty) "in"
   let resty ← LLVM.voidPtrType llvmctx
   let res ← buildPrologueAlloca builder (← LLVM.pointerType resty) "res"
+
+  let argcval ← LLVM.getParam main 0
+  let argvval ← LLVM.getParam main 1
+  let truncArgcval ← LLVM.buildSextOrTrunc builder argcval (← LLVM.i32Type llvmctx)
+  let argvval ← callLeanSetupLibUV builder truncArgcval argvval
+
   if usesLeanAPI then callLeanInitialize builder else callLeanInitializeRuntimeModule builder
     /- We disable panic messages because they do not mesh well with extracted closed terms.
         See issue #534. We can remove this workaround after we implement issue #467. -/
@@ -1501,8 +1516,6 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
         let _ ← LLVM.buildStore builder inv inslot
         let ity ← LLVM.size_tType llvmctx
         let islot ← buildPrologueAlloca builder ity "islot"
-        let argcval ← LLVM.getParam main 0
-        let argvval ← LLVM.getParam main 1
         LLVM.buildStore builder argcval islot
         buildWhile_ builder "argv"
           (condcodegen := fun builder => do

src/runtime/libuv.cpp

@@ -25,6 +25,10 @@ extern "C" void initialize_libuv() {
     lthread([]() { event_loop_run_loop(&global_ev); });
 }
 
+extern "C" LEAN_EXPORT char ** lean_setup_args(int argc, char ** argv) {
+    return uv_setup_args(argc, argv);
+}
+
 /* Lean.libUVVersionFn : Unit → Nat */
 extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg o) {
     return lean_unsigned_to_nat(uv_version());
@@ -38,5 +42,10 @@ extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg o) {
     return lean_box(0);
 }
 
+extern "C" LEAN_EXPORT char ** lean_setup_args(int argc, char ** argv) {
+    return argv;
+}
+
+
 #endif
 }

src/runtime/libuv.h

@@ -21,6 +21,7 @@ Author: Markus Himmel, Sofia Rodrigues
 namespace lean {
 
 extern "C" void initialize_libuv();
+extern "C" LEAN_EXPORT char ** lean_setup_args(int argc, char ** argv);
 
 // =======================================
 // General LibUV functions.