Failure state writing to broken pipe

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

In the tutorial implementation of Lean's cat version "feline" (Functional Programming in Lean, Section 2.4), it is claimed that the program can handle infinite streams. When I include it in a pipeline with an infinite stream (/dev/urandom here), however, I get a failure state:

# succeeds

$ lean --run feline.lean <( echo 'hello' )
hello

# fails; data is produced properly, but pipeline exits with error coming from the `lean` command.

$ lean --run feline.lean /dev/urandom | head -c 100 | tr -dc '[:alnum:]'
uncaught exception: resource vanished (error code: 32, broken pipe)
hqnvNaIQx3klM1NkwKgUHNx5jdo%

# succeeds with the same pipeline but /dev/urandom replaced by a normal file

$ lean --run feline.lean random_data | head -c 10 | tr -dc '[:alnum:]'
hRO%

Steps to Reproduce

1. In a linux system, create feline.lean with the tutorial code from Section 2.4 of Functional Programming in Lean. This should include the buffer variable bufsize and the functions dump (partial!), fileStream, process and main.

feline.lean:

def bufsize : USize := 20 * 1024

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    let stdout ← IO.getStdout
    stdout.write buf
    dump stream

def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
  let fileExists ← filename.pathExists
  if not fileExists then
    let stderr ← IO.getStderr
    stderr.putStrLn s!"File not found: {filename}"
    pure none
  else
    let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
    pure (some (IO.FS.Stream.ofHandle handle))

def process (exitCode : UInt32) (args : List String) : IO UInt32 := do
  match args with
  | [] => pure exitCode
  | "-" :: args =>
    let stdin ← IO.getStdin
    dump stdin
    process exitCode args
  | filename :: args =>
    let stream ← fileStream ⟨filename⟩
    match stream with
    | none =>
      process 1 args
    | some stream =>
      dump stream
      process exitCode args

def main (args : List String) : IO UInt32 :=
  match args with
  | [] => process 0 ["-"]
  | _ =>  process 0 args

2. Either build the program with lake or run directly with lean --run feline.lean

3. Feed a normal file to see that it works nominally:

$ lean --run feline.lean <( echo 'hi' )
hi

5. Run lean --run feline.lean /dev/urandom | head -c 100 > random_data in a writable directory to get the error state.

Expected behavior: The pipeline terminates successfully and the new file random_data contains 100 random bytes.

Actual behavior: The pipeline terminates with non-zero exit code, and the message uncaught exception: resource vanished (error code: 32, broken pipe) is put in stderr. The file random_data has been created and does contain 100 random bytes.

Reproduces how often: This behavior is constant.

Versions

Lean version : Lean (version 4.0.0, commit 7dbfaf9b7519, Release)
OS : Linux ArchSys 6.1.1-arch1-1 #1 SMP PREEMPT_DYNAMIC Wed, 21 Dec 2022 22:27:55 +0000 x86_64 GNU/Linux

Additional Information

I wonder if this issue is in any way related to issue #349.

Start by reproducing the pipeline with the tutorial's feline.lean, especially dump, process, and the stdout.write call, using /dev/urandom piped to head. Trace how the broken-pipe error becomes an uncaught exception; done means the pipeline exits successfully without the stderr error while still producing the requested output.