IO.Process.output hangs on large input strings

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

If a child process (say cat) called by IO.Process.output is sent a large
number of bytes (say 196K + 1 bytes on Linux), then the capacity of the
pipes fill up and the program deadlocks.

Context

Chat
This occurred when I was calling a program with several megabytes of data. When looking into the problem, I found two more issues that I will submit separately.

1. IO.Process.output/IO.Process.run can continue after throwing an error. This is easily triggered by the underlying process sending byte 255 and then closing standard error. If the programmer thinks some untrusted code is no longer running when it still is, that could be very bad (Bug #14001).
2. IO.Process.run fails if the stdout or stderr is not UTF8. This is caused because it calls IO.Process.output that returns its stdout and stderr as strings (Bug #14003).

I think that a part of the solution is to create a IO.Process.binOutput, that I will propose separately.

Steps to Reproduce

Run the following code on a Linux machine with 64K buffers.

To determine the pipe capacity on your Linux system, you can run the following command:

dd if=/dev/zero bs=1 | sleep 999

Wait a few seconds, hit control-C, and observe how many bytes were produced.

Save the following into a file, say Test.lean.

def testProcessOutputWithCatSize (numBytes : Nat) : IO Unit := do
  IO.println s!"Testing running cat with string of size {numBytes}"
  let input := String.ofList (List.replicate numBytes 'a') -- A string of length numBytes.
  let spawnArgs : IO.Process.SpawnArgs := { cmd := "cat", args := #[] }
  let startTime ← IO.monoNanosNow
  let out ← IO.Process.output spawnArgs (some input)
  let endTime ← IO.monoNanosNow
  if out.exitCode == 0 && out.stdout.trimAscii == input && out.stderr == "" then
    let duration := (Float.ofNat (endTime - startTime)) / 1_000_000_000.0
    IO.println s!"SUCCESS: Passed in {duration} seconds."
  else
    IO.println "FAILURE: Failed."
    return

#version

def main(_args : List String) : IO Unit := do
  testProcessOutputWithCatSize 1000000

Then, run lean --run Test.lean.

Expected behavior:
It should run to completion in well under a second.

Actual behavior:
It hangs forever. Note that reducing the number of bytes to a smaller value
makes the problem vanish.

Versions

Lean 4.32.0-nightly-2026-06-10
Linux, with a 64K pipe buffer.

Additional Information

Impact

This impacts both IO.Process.output and IO.Process.run (that calls
IO.Process.output).

Proposed Solution: In IO.Process.output, the main process writes data into the stdin of the child process. If this were done as a task, the issue would be resolved. If this is done as a dedicated task, it will not affect the thread maximum, but of course that is one more thread for the kernel to handle.

Start with the IO.Process.output and IO.Process.run entry points, then run the reproducer in Test.lean on Linux with a large input such as 1,000,000 bytes. Trace how input is written while stdout and stderr are collected. Done means the test completes without hanging, returns exit code 0, and preserves the expected stdout and empty stderr.