Failure state writing to broken pipe

[ykonstant1]

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.

[Kha]

On second glance the failure is exactly as desired: leaving stdin broken is what head does after all.

$ cat /dev/urandom | head -n1 > /dev/null
$ echo $pipestatus
141 0

So the only deviation from a standard C program is the display of the error message, as well as the exact exit code, which stems from handling SIGPIPE. Whether that is the right default appears to be a hard question, but at the very least there should be a way to opt out of it.

[ykonstant1]

Ooh, I see! That is... interesting. I will have to ask at a unix forum for more information about the design decisions that led to this phenomenon. If you have a program that handles SIGPIPE this way embedded in a shell script that uses something like pipefail or set -e, you will get unexpected aborts...

I am not sure how to tag this issue, now; it is not a Lean bug, but maybe something to keep in mind?

[Kha]

pipefail seems problematic using either SIGPIPE approach

$ (set -o pipefail; cat /dev/urandom | head -n1 > /dev/null); echo $?
141