feat: generalize Process.output/run to allow an input

src/Init/System/IO.lean

@@ -1476,13 +1476,21 @@ structure Output where
   stderr   : String
 
 /--
-Runs a process to completion and captures its output and exit code. The child process is run with a
-null standard input, and the current process blocks until it has run to completion.
+Runs a process to completion and captures its output and exit code.
+The child process is run with a null standard input or the specified input if provided,
+and the current process blocks until it has run to completion.
 
 The specifications of standard input, output, and error handles in `args` are ignored.
 -/
-def output (args : SpawnArgs) : IO Output := do
-  let child ← spawn { args with stdout := .piped, stderr := .piped, stdin := .null }
+def output (args : SpawnArgs) (input? : Option String := none) : IO Output := do
+  let child ←
+    if let some input := input? then
+      let (stdin, child) ← (← spawn { args with stdout := .piped, stderr := .piped, stdin := .piped }).takeStdin
+      stdin.putStr input
+      stdin.flush
+      pure child
+    else
+      spawn { args with stdout := .piped, stderr := .piped, stdin := .null }
   let stdout ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated
   let stderr ← child.stderr.readToEnd
   let exitCode ← child.wait
@@ -1490,12 +1498,15 @@ def output (args : SpawnArgs) : IO Output := do
   pure { exitCode := exitCode, stdout := stdout, stderr := stderr }
 
 /--
-Runs a process to completion, blocking until it terminates. If the child process terminates
-successfully with exit code 0, its standard output is returned. An exception is thrown if it
-terminates with any other exit code.
+Runs a process to completion, blocking until it terminates.
+The child process is run with a null standard input or the specified input if provided,
+If the child process terminates successfully with exit code 0, its standard output is returned.
+An exception is thrown if it terminates with any other exit code.
+
+The specifications of standard input, output, and error handles in `args` are ignored.
 -/
-def run (args : SpawnArgs) : IO String := do
-  let out ← output args
+def run (args : SpawnArgs) (input? : Option String := none) : IO String := do
+  let out ← output args input?
   if out.exitCode != 0 then
     throw <| IO.userError s!"process '{args.cmd}' exited with code {out.exitCode}\
       \nstderr:\