The Lean Language Reference

15.9. Processes🔗

15.9.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 α

Terminates the current process with the provided exit code. 0 indicates success, all other values indicate failure.

🔗opaque
IO.Process.getPID : BaseIO UInt32

Returns the process ID of the calling process.

15.9.2. Running Processes

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

  1. 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.

  2. 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.

  3. 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

Runs a process to completion, blocking until it terminates. If the child process terminates successfully with exit code 0, its standard output is returned. An exception is thrown if it terminates with any other exit code.

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

Runs a process to completion and captures its output and exit code. The child process is run with a null standard input, and the current process blocks until it has run to completion.

The specifications of standard input, output, and error handles in args are ignored.

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)

Starts a child process with the provided configuration. The child process is spawned using operating system primitives, and it can be written in any language.

The child process runs in parallel with the parent.

If the child process's standard input is a pipe, use IO.Process.Child.takeStdin to make it possible to close the child's standard input before the process terminates, which provides the child with an end-of-file marker.

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

Configuration for a child process to be spawned.

Use IO.Process.spawn to start the child process. IO.Process.output and IO.Process.run can be used when the child process should be run to completion, with its output and/or error code captured.

Constructor

IO.Process.SpawnArgs.mk

Extends

Fields

stdin : IO.Process.Stdio
Inherited from
  1. IO.Process.StdioConfig
stdout : IO.Process.Stdio
Inherited from
  1. IO.Process.StdioConfig
stderr : IO.Process.Stdio
Inherited from
  1. IO.Process.StdioConfig
cmd : String

Command name.

args : Array String

Arguments for the command.

cwd : Option System.FilePath

The child process's working directory. Inherited from the parent current process if none.

env : Array (String × Option String)

Add or remove environment variables for the child process.

The child process inherits the parent's environment, as modified by env. Keys in the array are the names of environment variables. A none, causes the entry to be removed from the environment, and some sets the variable to the new value, adding it if necessary. Variables are processed from left to right.

setsid : Bool

Starts the child process in a new session and process group using setsid. Currently a no-op on non-POSIX platforms.

🔗structure
IO.Process.StdioConfig : Type

Configuration for the standard input, output, and error handles of a child process.

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

Whether the standard input, output, and error handles of a child process should be attached to pipes, inherited from the parent, or null.

If the stream is a pipe, then the parent process can use it to communicate with the child.

Constructors

piped : IO.Process.Stdio

The stream should be attached to a pipe.

inherit : IO.Process.Stdio

The stream should be inherited from the parent process.

null : IO.Process.Stdio

The stream should be empty.

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

The type of handles that can be used to communicate with a child process on its standard input, output, or error streams.

For IO.Process.Stdio.piped, this type is IO.FS.Handle. Otherwise, it is Unit, because no communication is possible.

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

A child process that was spawned with configuration cfg.

The configuration determines whether the child process's standard input, standard output, and standard error are IO.FS.Handles or Unit.

Constructor

IO.Process.Child.mk

Fields

stdin : cfg.stdin.toHandleType

The child process's standard input handle, if it was configured as IO.Process.Stdio.piped, or () otherwise.

stdout : cfg.stdout.toHandleType

The child process's standard output handle, if it was configured as IO.Process.Stdio.piped, or () otherwise.

stderr : cfg.stderr.toHandleType

The child process's standard error handle, if it was configured as IO.Process.Stdio.piped, or () otherwise.

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

Blocks 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)

Checks whether the child has exited. Returns none if the process has not exited, or its exit code if it has.

🔗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 })

Extracts the stdin field from a Child object, allowing the handle to be closed while maintaining a reference to the child process.

File handles are closed when the last reference to them is dropped. Closing the child's standard input causes an end-of-file marker. Because the Child object has a reference to the standard input, this operation is necessary in order to close the stream while the process is running (e.g. to extract its exit code after calling Child.wait). Many processes do not terminate until their standard input is exhausted.

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

The result of running a process to completion.

Constructor

IO.Process.Output.mk

Fields

exitCode : UInt32

The process's exit code.

stdout : String

Everything that was written to the process's standard output.

stderr : String

Everything that was written to the process's standard error.