IO.Process.output can throw an error while the underlying spawned process is still running

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

When calling IO.Process.output on a program that closes stderr early, the program
can continue to run after IO.Process.output has thrown an exception.
This also impacts IO.Process.run.

Context

#lean4 > Fixing IO.Process.output and IO.Process.run with binOutput

I noticed this bug when analyzing Bug #14000. There is also another issue,
that IO.Process.run should not be failing at all in this scenario (Bug #14003).

Steps to Reproduce

First, we create a bad_stderr.c file that:

• writes (and flushes) an invalid UTF8 byte sequence (the byte 255) to standard error,
• closes stderr.
• Sleeps for ten seconds.

#include <stdio.h>
#include <unistd.h>
#include <sys/time.h>

int main(int argc, char** argv) {
  // Write invalid UTF-8 byte
  fputc(0xff, stderr);
  fflush(stderr);
  // Close standard error
  fclose(stderr);
  // Sleep for 10 seconds
  sleep(10);
  // Write "Hello world!" to stdout.
  return 0;
}

Call g++ bad_stderr.c to compile to a.out.

File Test.lean follows:

#version

def main(_args : List String) : IO Unit := do
  IO.println s!"Testing running bad_stderr with IO.Process.output"
  let spawnArgs : IO.Process.SpawnArgs := { cmd := "./a.out", args := #[] }
  let startTime ← IO.monoNanosNow
  try
    let out ← IO.Process.output spawnArgs none
    let endTime ← IO.monoNanosNow
    let duration := (Float.ofNat (endTime - startTime)) / 1_000_000_000.0
    IO.println s!"FAILURE: Where is the exception? exitCode={out.exitCode} stdout.length={out.stdout.length} stderr.length={out.stderr.length} in {duration} seconds."
  catch e =>
    let endTime ← IO.monoNanosNow
    let duration := (Float.ofNat (endTime - startTime)) / 1_000_000_000.0
    if (duration < 9.0) then
      IO.println s!"FAILURE: Caught exception {e} in {duration} seconds. Should have waited at least ten seconds."
    else
      IO.println s!"SUCCESS: Caught exception {e} in {duration} seconds. Waited long enough for the program to finish."

Run the Lean code with lean --run Test.lean.

Expected behavior: Should print out SUCCESS. IO.Process.output should throw an error, but only after the process has completed (so at least 9 seconds).

Actual behavior: Throws an error before the process has completed.

FAILURE: Caught exception Tried to read from handle containing non UTF-8 data. in 0.006252 seconds. Should have waited at least ten seconds.

Versions

Lean 4.32.0-nightly-2026-06-10
Linux

Additional Information

None.

Impact

This can lead to a programmer believing that a subprocess was finished when it was still running. The bad_stderr.c sleeps for ten seconds and does nothing, but it could start writing or reading files at this point. For example, a programmer has a reasonable expectation if they run different programs sequentially using IO.Process.run, then they will be run in sequence, when in fact they will be run in parallel.

I believe that there are security implications here.

Solution: have a IO.Process.binOutput and IO.Process.BinOutput that work with byte arrays (see separate RFC). Convert to UTF8 in the main thread, avoiding the timing issues. Note issue #14000 about hanging.

Note that the IO.Process.run has no need to call IO.Process.output (see next issue): instead, it should call IO.Process.binOutput directly.

Start by reproducing the issue with bad_stderr.c and Test.lean, using the IO.Process.output and IO.Process.run entry points described here. Trace how stderr decoding errors are propagated relative to process completion, and compare the behavior with the proposed binOutput approach. Done means an error is not returned until the spawned process has finished.