Can Lean close a stdin Handle?

Stream: lean4

[Mirek Olšák]

I wanted Lean to do some process communication, and I am not able to finish the data stream. It is especially annoying when the passed data would be binary. As a test, let's say we have this Lean code

import Lean.Elab.Command

def tryPipe : Lean.Elab.Command.CommandElabM Unit := do
  let args : IO.Process.SpawnArgs := {
    cmd := "./try_pipe.py",
    args := #[],
    stdin := .piped,
    stdout := .piped,
    stderr := .piped
  }
  let process ← IO.Process.spawn args
  process.stdin.putStr "hello\n"
  process.stdin.putStr "pipe\n"
  process.stdin.flush
  -- close finish stop somehow !
  let stdout ← IO.asTask process.stdout.readToEnd .dedicated
  let _ ← IO.asTask process.stderr.readToEnd
  let _ ← process.wait
  let result ← IO.ofExcept stdout.get
  Lean.logInfo result

run_cmd tryPipe

calling this Python code

#!/usr/bin/python

import sys

data = sys.stdin.read()
# data = sys.stdin.readline()
print("<data>")
print(data, end='')
print("</data>")

I found a post from 2021 / 2022 that it was not possible. Did anything change since then?

[Yann Herklotz]

You might be looking for takeStdin. The docstring of the function states that it closes the file handle when there are no more references to it, which seems to have the behaviour you are looking for:

import Lean.Elab.Command

def tryPipe : Lean.Elab.Command.CommandElabM Unit := do
  let args : IO.Process.SpawnArgs := {
    cmd := "./try_pipe.py",
    args := #[],
    stdin := .piped,
    stdout := .piped,
    stderr := .piped
  }
  let process ← IO.Process.spawn args
  let (stdinHandle, newChild) ← process.takeStdin
  stdinHandle.putStr "hello\n"
  stdinHandle.putStr "pipe\n"
  stdinHandle.flush
  -- close finish stop somehow !
  let stdout ← IO.asTask newChild.stdout.readToEnd .dedicated
  let _ ← IO.asTask newChild.stderr.readToEnd
  let _ ← newChild.wait
  let result ← IO.ofExcept stdout.get
  Lean.logInfo result

run_cmd tryPipe

[Mirek Olšák]

thanks, magic :-)

[Eric Wieser]

(docs#IO.Process.Child.takeStdin)