IO.Process.run throws an error on non-UTF8 stdout or stderr.

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

IO.Process.run fails if the stdout or stderr are not valid UTF8
(e.g. a single byte 0xff).

Context

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

When trying to figure out Bug #14000, I discovered Bug #14001 and this
one. I have a solution using IO.Process.binOutput (code to be written).

Steps to Reproduce

This program writes an invalid UTF8 byte sequence (the byte 255) to standard error.

bad_stderr2.c follows:

#include <stdio.h>

int main(int argc, char** argv) {
  // Write invalid UTF-8 byte
  fputc(0xff, stderr);
  return 0;
}

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

File Test.lean follows:

def main(_args : List String) : IO Unit := do
  IO.println s!"Testing IO.Process.run bad_stderr2.c"
  let spawnArgs : IO.Process.SpawnArgs := { cmd := "./a.out", args := #[] }
  let _ ← IO.Process.run spawnArgs

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

Expected behavior:

To return with no error.

Actual behavior:

Throws an error:

Uncaught exception: Tried to read from handle containing non UTF-8 data.

Versions

Lean 4.32.0-nightly-2026-06-10

Linux

Additional Information

None

Impact

IO.Process.run only works when stdout and stderr are valid UTF8.
If it were fixed, then it could be used to run programs that print arbitrary
binary data to stdout or stderr.

Solution: have a IO.Process.binOutput and IO.Process.BinOutput that work with byte arrays. Then, have IO.Process.run work on top of that, so that no string
conversion happens at all.

Start by running the supplied bad_stderr2.c and Test.lean reproducer to confirm that IO.Process.run rejects the invalid byte. Read the IO.Process.run and IO.Process.binOutput entry points described in the issue, then trace how stdout and stderr are converted. Done means IO.Process.run completes when the child emits non-UTF8 output, without string conversion errors.