external process

Stream: lean4

[Alexandre Rademaker]

How can I call an external process and get its output to be parsed in Lean4? Is there anything similar to https://hackage.haskell.org/package/process-1.6.7.0/docs/System-Process.html#v:createProcess ?

[Wojciech Nawrocki]

Does docs4#IO.Process.spawn and the related methods help?

[Max Nowak 🐉]

I use the following code:

import Init.System.IO
open IO.Process

/-- Pipe input into stdin of the spawned process, then return output upon completion. -/
def cmd_with_stdin (args : SpawnArgs) (input : String) : IO Output := do
  let child <- spawn { args with stdin := .piped, stdout := .piped, stderr := .piped }
  let (stdin, child) <- child.takeStdin
  stdin.putStr input
  stdin.flush
  let stdout <- IO.asTask child.stdout.readToEnd Task.Priority.dedicated
  let stderr <- child.stderr.readToEnd
  let exitCode <- child.wait
  let stdout <- IO.ofExcept stdout.get
  return { exitCode, stdout, stderr }