8.8. Processes

8.8.1. Current Process

opaque

IO.Process.getCurrentDir : IO System.FilePath

Returns the current working directory of the calling process.

opaque

IO.Process.setCurrentDir
    (path : System.FilePath) : IO Unit

Sets the current working directory of the calling process.

opaque

IO.Process.exit {α : Type} : UInt8 → IO α

opaque

IO.Process.getPID : BaseIO UInt32

Returns the process ID of the calling process.

8.8.2. Running Processes

There are three primary ways to run other programs from Lean:

IO.Process.run synchronously executes another program, returning its standard output as a string. It throws an error if the process exits with an error code other than 0.
IO.Process.output synchronously executes another program with an empty standard input, capturing its standard output, standard error, and exit code. No error is thrown if the process terminates unsuccessfully.
IO.Process.spawn starts another program asynchronously and returns a data structure that can be used to access the process's standard input, output, and error streams.

def

IO.Process.run (args : IO.Process.SpawnArgs)
    : IO String

Run process to completion and return stdout on success.

Running a Program

When run, this program concatenates its own source code with itself twice using the Unix tool cat.

def main : IO Unit := do
  let src2 ← IO.Process.run {cmd := "cat", args := #["Main.lean", "Main.lean"]}
  IO.println src2
-- Main.lean ends here

Its output is:

                stdout-- Main.lean begins heredef main : IO Unit := do  let src2 ← IO.Process.run {cmd := "cat", args := #["Main.lean", "Main.lean"]}  IO.println src2-- Main.lean ends here-- Main.lean begins heredef main : IO Unit := do  let src2 ← IO.Process.run {cmd := "cat", args := #["Main.lean", "Main.lean"]}  IO.println src2-- Main.lean ends here

Running a Program on a File

This program uses the Unix utility grep as a filter to find four-digit palindromes. It creates a file that contains all numbers from 0 through 9999, and then invokes grep on it, reading the result from its standard output.

def main : IO Unit := do
  -- Feed the input to the subprocess
  IO.FS.withFile "numbers.txt" .write fun h =>
    for i in [0:10000] do
      h.putStrLn (toString i)

  let palindromes ← IO.Process.run {
    cmd := "grep",
    args := #[r#"^\([0-9]\)\([0-9]\)\2\1$"#, "numbers.txt"]
  }

  let count := palindromes.trim.splitOn "\n" |>.length

  IO.println s!"There are {count} four-digit palindromes."

Its output is:

stdoutThere are 90 four-digit palindromes.

def

IO.Process.output (args : IO.Process.SpawnArgs)
    : IO IO.Process.Output

Run process to completion and capture output. The process does not inherit the standard input of the caller.

Checking Exit Codes

When run, this program first invokes cat on a nonexistent file and displays the resulting error code. It then concatenates its own source code with itself twice using the Unix tool cat.

def main : IO UInt32 := do
  let src1 ← IO.Process.output {cmd := "cat", args := #["Nonexistent.lean"]}
  IO.println s!"Exit code from failed process: {src1.exitCode}"

  let src2 ← IO.Process.output {cmd := "cat", args := #["Main.lean", "Main.lean"]}
  if src2.exitCode == 0 then
    IO.println src2.stdout
  else
    IO.eprintln "Concatenation failed"
    return 1

  return 0
-- Main.lean ends here

Its output is:

                stdoutExit code from failed process: 1-- Main.lean begins heredef main : IO UInt32 := do  let src1 ← IO.Process.output {cmd := "cat", args := #["Nonexistent.lean"]}  IO.println s!"Exit code from failed process: {src1.exitCode}"  let src2 ← IO.Process.output {cmd := "cat", args := #["Main.lean", "Main.lean"]}  if src2.exitCode == 0 then    IO.println src2.stdout  else    IO.eprintln "Concatenation failed"    return 1  return 0-- Main.lean ends here-- Main.lean begins heredef main : IO UInt32 := do  let src1 ← IO.Process.output {cmd := "cat", args := #["Nonexistent.lean"]}  IO.println s!"Exit code from failed process: {src1.exitCode}"  let src2 ← IO.Process.output {cmd := "cat", args := #["Main.lean", "Main.lean"]}  if src2.exitCode == 0 then    IO.println src2.stdout  else    IO.eprintln "Concatenation failed"    return 1  return 0-- Main.lean ends here

opaque

IO.Process.spawn (args : IO.Process.SpawnArgs)
    : IO (IO.Process.Child args.toStdioConfig)

Asynchronous Subprocesses

This program uses the Unix utility grep as a filter to find four-digit palindromes. It feeds all numbers from 0 through 9999 to the grep process and then reads its result. This code is only correct when grep is sufficiently fast and when the output pipe is large enough to contain all 90 four-digit palindromes.

def main : IO Unit := do
  let grep ← IO.Process.spawn {
    cmd := "grep",
    args := #[r#"^\([0-9]\)\([0-9]\)\2\1$"#],
    stdin := .piped,
    stdout := .piped,
    stderr := .null
  }

  -- Feed the input to the subprocess
  for i in [0:10000] do
    grep.stdin.putStrLn (toString i)

  -- Consume its output, after waiting 100ms for grep to process the data.
  IO.sleep 100
  let count := (← grep.stdout.readToEnd).trim.splitOn "\n" |>.length

  IO.println s!"There are {count} four-digit palindromes."

Its output is:

stdoutThere are 90 four-digit palindromes.

structure

IO.Process.SpawnArgs : Type

Constructor

IO.Process.SpawnArgs.mk

Extends

IO.Process.StdioConfig

Fields

`stdin`	`:`	`IO.Process.Stdio`
		Inherited from `IO.Process.StdioConfig`
`stdout`	`:`	`IO.Process.Stdio`
		Inherited from `IO.Process.StdioConfig`
`stderr`	`:`	`IO.Process.Stdio`
		Inherited from `IO.Process.StdioConfig`
`cmd`	`:`	`String`
		Command name.
`args`	`:`	`Array String`
		Arguments for the process
`cwd`	`:`	`Option System.FilePath`
		Working directory for the process. Inherit from current process if `none`.
`env`	`:`	`Array (String × Option String)`
		Add or remove environment variables for the process.
`setsid`	`:`	`Bool`
		Start process in new session and process group using `setsid`. Currently a no-op on non-POSIX platforms.

structure

IO.Process.StdioConfig : Type

Constructor

IO.Process.StdioConfig.mk

Fields

`stdin`	`:`	`IO.Process.Stdio`
		Configuration for the process' stdin handle.
`stdout`	`:`	`IO.Process.Stdio`
		Configuration for the process' stdout handle.
`stderr`	`:`	`IO.Process.Stdio`
		Configuration for the process' stderr handle.

inductive type

IO.Process.Stdio : Type

Constructors

piped : IO.Process.Stdio
inherit : IO.Process.Stdio
null : IO.Process.Stdio

def

IO.Process.Stdio.toHandleType
    : IO.Process.Stdio → Type

structure

IO.Process.Child (cfg : IO.Process.StdioConfig)
    : Type

Constructor

IO.Process.Child.mk

Fields

`stdin`	`:`	`cfg.stdin.toHandleType`
`stdout`	`:`	`cfg.stdout.toHandleType`
`stderr`	`:`	`cfg.stderr.toHandleType`

opaque

IO.Process.Child.wait
    {cfg : IO.Process.StdioConfig}
    : IO.Process.Child cfg → IO UInt32

Block until the child process has exited and return its exit code.

opaque

IO.Process.Child.tryWait
    {cfg : IO.Process.StdioConfig}
    : IO.Process.Child cfg → IO (Option UInt32)

Check whether the child has exited yet. If it hasn't return none, otherwise its exit code.

opaque

IO.Process.Child.kill
    {cfg : IO.Process.StdioConfig}
    : IO.Process.Child cfg → IO Unit

Terminates the child process using the SIGTERM signal or a platform analogue. If the process was started using SpawnArgs.setsid, terminates the entire process group instead.

opaque

IO.Process.Child.takeStdin
    {cfg : IO.Process.StdioConfig}
    : IO.Process.Child cfg →
      IO
        (cfg.stdin.toHandleType ×
          IO.Process.Child
            { stdin := IO.Process.Stdio.null,
              stdout := cfg.stdout,
              stderr := cfg.stderr })

Extract the stdin field from a Child object, allowing them to be freed independently. This operation is necessary for closing the child process' stdin while still holding on to a process handle, e.g. for Child.wait. A file handle is closed when all references to it are dropped, which without this operation includes the Child object.

Closing a Subprocess's Standard Input

This program uses the Unix utility grep as a filter to find four-digit palindromes, ensuring that the subprocess terminates successfully. It feeds all numbers from 0 through 9999 to the grep process, then closes the process's standard input, which causes it to terminate. After checking grep's exit code, the program extracts its result.

def main : IO UInt32 := do
  let grep ← do
    let (stdin, child) ← (← IO.Process.spawn {
      cmd := "grep",
      args := #[r#"^\([0-9]\)\([0-9]\)\2\1$"#],
      stdin := .piped,
      stdout := .piped,
      stderr := .null
    }).takeStdin

    -- Feed the input to the subprocess
    for i in [0:10000] do
      stdin.putStrLn (toString i)

    -- Return the child without its stdin handle.
    -- This closes the handle, because there are
    -- no more references to it.
    pure child

  -- Wait for grep to terminate
  if (← grep.wait) != 0 then
    IO.eprintln s!"grep terminated unsuccessfully"
    return 1

  -- Consume its output
  let count := (← grep.stdout.readToEnd).trim.splitOn "\n" |>.length

  IO.println s!"There are {count} four-digit palindromes."
  return 0

Its output is:

stdoutThere are 90 four-digit palindromes.

structure

IO.Process.Output : Type

Constructor

IO.Process.Output.mk

Fields

`exitCode`	`:`	`UInt32`
`stdout`	`:`	`String`
`stderr`	`:`	`String`