21.9. 流程🔗

21.9.1. 当前流程🔗

opaque

IO.Process.getCurrentDir : IO System.FilePath
IO.Process.getCurrentDir :
  IO System.FilePath

Returns the current working directory of the calling process.

opaque

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

Sets the current working directory of the calling process.

opaque

IO.Process.exit {α : Type} : UInt8 → IO α
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
IO.Process.getPID : BaseIO UInt32

Returns the process ID of the calling process.

21.9.2. 正在运行的进程🔗

从 Lean 运行其他程序有三种主要方法：

IO.Process.run 同步执行另一个程序，以字符串形式返回其标准输出。如果进程退出时出现 0 以外的错误代码，则会引发错误。
IO.Process.output 同步执行另一个具有空标准输入的程序，捕获其标准输出、标准错误和退出代码。如果进程终止失败，则不会引发任何错误。
IO.Process.spawn 异步启动另一个程序并返回可用于访问进程的标准输入、输出和错误流的数据结构。

def

IO.Process.run (args : IO.Process.SpawnArgs)
  (input? : Option String := none) : IO String
IO.Process.run
  (args : IO.Process.SpawnArgs)
  (input? : Option String := none) :
  IO String

Runs a process to completion, blocking until it terminates. The child process is run with a null standard input or the specified input if provided, 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.

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

Running a Program

运行时，该程序使用 Unix 工具 cat 将其自己的源代码与自身连接两次。

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

其输出为：

                    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

该程序使用 Unix 实用程序 grep 作为过滤器来查找四位数字回文。它创建一个包含从 0 到 9999 的所有数字的文件，然后对其调用 grep，从其标准输出读取结果。

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.trimAscii.split "\n" |>.length

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

其输出为：

stdoutThere are 90 four-digit palindromes.

def

IO.Process.output (args : IO.Process.SpawnArgs)
  (input? : Option String := none) : IO IO.Process.Output
IO.Process.output
  (args : IO.Process.SpawnArgs)
  (input? : Option String := none) :
  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 or the specified input if provided, 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

运行时，该程序首先对不存在的文件调用 cat 并显示生成的错误代码。然后，它使用 Unix 工具 cat 将自己的源代码与自身连接两次。

-- Main.lean begins here
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

其输出为：

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

该程序使用 Unix 实用程序 grep 作为过滤器来查找四位数字回文。它将从 0 到 9999 的所有数字提供给 grep 进程，然后读取其结果。仅当 grep 足够快并且输出管道足够大以包含所有 90 个四位数字回文时，此代码才是正确的。

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).trimAscii.split "\n" |>.length

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

其输出为：

stdoutThere are 90 four-digit palindromes.

structure

IO.Process.SpawnArgs : Type
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

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

inheritEnv : Bool

Inherit environment variables from the spawning process.

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

IO.Process.Stdio.piped : IO.Process.Stdio

The stream should be attached to a pipe.

IO.Process.Stdio.inherit : IO.Process.Stdio

The stream should be inherited from the parent process.

IO.Process.Stdio.null : IO.Process.Stdio

The stream should be empty.

def

IO.Process.Stdio.toHandleType : IO.Process.Stdio → Type
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
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.

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
IO.Process.Child.wait
  {cfg : IO.Process.StdioConfig} :
  IO.Process.Child cfg → IO UInt32

Blocks until the child process has exited and returns its exit code.

opaque

IO.Process.Child.tryWait {cfg : IO.Process.StdioConfig} :
  IO.Process.Child cfg → IO (Option UInt32)
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
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 })
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

该程序使用 Unix 实用程序 grep 作为过滤器来查找四位数回文，确保子进程成功终止。它将从 0 到 9999 的所有数字提供给 grep 进程，然后关闭进程的标准输入，从而导致其终止。检查 grep 的退出代码后，程序提取其结果。

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).trimAscii.split "\n" |>.length

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

其输出为：

stdoutThere are 90 four-digit palindromes.

structure

IO.Process.Output : Type
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.