feat: IO.Process.Child.takeStdin

src/Init/System/IO.lean

@@ -424,6 +424,15 @@ structure Child (cfg : StdioConfig) where
 
 @[extern "lean_io_process_child_wait"] constant Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32
 
+/--
+Extract the `stdin` field from a `Child` object, allowing them to be freed independently.
+This operation is necessary for closing the child process' stdin while still holding on to a process handle,
+e.g. for `Child.wait`. A file handle is closed when all references to it are dropped, which without this
+operation includes the `Child` object.
+-/
+@[extern "lean_io_process_child_take_stdin"] constant Child.takeStdin {cfg : @& StdioConfig} : Child cfg →
+    IO (cfg.stdin.toHandleType × Child { cfg with stdin := Stdio.null })
+
 structure Output where
   exitCode : UInt32
   stdout   : String

src/runtime/process.cpp

@@ -202,6 +202,13 @@ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const &
     return lean_io_result_mk_ok(r.steal());
 }
 
+extern "C" obj_res lean_io_process_child_take_stdin(b_obj_arg, obj_arg lchild, obj_arg) {
+    object_ref child(lchild);
+    object_ref child2 = mk_cnstr(0, object_ref(box(0)), cnstr_get_ref(child, 1), cnstr_get_ref(child, 2), cnstr_get_ref(child, 3));
+    object_ref r = mk_cnstr(0, cnstr_get_ref(child, 0), child2);
+    return lean_io_result_mk_ok(r.steal());
+}
+
 void initialize_process() {
     g_win_handle_external_class = lean_register_external_class(win_handle_finalizer, win_handle_foreach);
 }
@@ -332,6 +339,14 @@ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const &
     return lean_io_result_mk_ok(r.steal());
 }
 
+extern "C" obj_res lean_io_process_child_take_stdin(b_obj_arg, obj_arg lchild, obj_arg) {
+    object_ref child(lchild);
+    object_ref child2 = mk_cnstr(0, object_ref(box(0)), cnstr_get_ref(child, 1), cnstr_get_ref(child, 2), sizeof(pid_t));
+    cnstr_set_uint32(child2.raw(), 3 * sizeof(object *), cnstr_get_uint32(child.raw(), 3 * sizeof(object *)));
+    object_ref r = mk_cnstr(0, cnstr_get_ref(child, 0), child2);
+    return lean_io_result_mk_ok(r.steal());
+}
+
 void initialize_process() {}
 void finalize_process() {}
 

tests/lean/Process.lean

@@ -47,3 +47,13 @@ def usingIO {α} (x : IO α) : IO α := x
 #eval usingIO do
   let child ← spawn { cmd := "sh", args := #["-c", "echo nullStderr >& 2"], stderr := Stdio.null };
   child.wait
+
+#eval usingIO do
+  let lean ← IO.Process.spawn {
+    cmd := "lean",
+    args := #["--stdin"]
+    stdin := IO.Process.Stdio.piped
+  }
+  let (stdin, lean) ← lean.takeStdin
+  stdin.putStr "#exit\n"
+  lean.wait

tests/lean/Process.lean.expected.out

@@ -9,3 +9,4 @@ flush of broken pipe failed
 0
 0
 0
+0