Lean 语言参考手册

21.9. 进程🔗

21.9.1. 当前进程🔗

🔗不透明定义
IO.Process.getCurrentDir : IO System.FilePath
IO.Process.getCurrentDir :
  IO System.FilePath

返回调用进程的当前工作目录。

🔗不透明定义
IO.Process.setCurrentDir (path : System.FilePath) : IO Unit
IO.Process.setCurrentDir
  (path : System.FilePath) : IO Unit

设置调用进程的当前工作目录。

🔗不透明定义
IO.Process.exit {α : Type} : UInt8 → IO α
IO.Process.exit {α : Type} : UInt8 → IO α

以给定退出码终止当前进程。0 表示成功，其他所有值都表示失败。

🔗不透明定义
IO.Process.getPID : BaseIO UInt32
IO.Process.getPID : BaseIO UInt32

返回调用进程的进程 ID。

21.9.2. 运行进程🔗

在 Lean 中运行其他程序主要有三种方式：

  1. IO.Process.run 同步执行另一个程序，并以字符串形式返回其标准输出。若该进程以非 0 退出码退出，它会抛出错误。

  2. IO.Process.output 以空标准输入同步执行另一个程序，并捕获其标准输出、标准错误和退出码。即使进程执行失败，也不会抛出错误。

  3. IO.Process.spawn 异步启动另一个程序，并返回一个可访问该进程标准输入流、标准输出流和标准错误流的数据结构。

🔗定义
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

运行一个进程直到完成，并阻塞等待其终止。 子进程使用空标准输入运行；如果提供了输入，则使用指定输入。 如果子进程以退出码 0 成功终止，则返回其标准输出。 若以任何其他退出码终止，则抛出异常。

args 中对标准输入、输出和错误句柄的指定会被忽略。

运行程序

运行时，该程序使用 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
对文件运行程序

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

def main : IO Unit := do -- 向子进程提供输入 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.
🔗定义
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

运行一个进程直到完成，并捕获其输出和退出码。 子进程使用空标准输入运行；如果提供了输入，则使用指定输入， 当前进程会阻塞直到它运行完毕。

args 中对标准输入、输出和错误句柄的指定会被忽略。

检查退出码

运行时，该程序先对一个不存在的文件调用 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
🔗不透明定义
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)

使用给定配置启动一个子进程。子进程通过操作系统原语生成，因此可以用任何语言编写。

子进程与父进程并行运行。

如果子进程的标准输入是管道，请使用 IO.Process.Child.takeStdin，这样就能在进程终止前关闭子进程的标准输入，从而向子进程提供一个文件结束标记。

异步子进程

该程序使用 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 } -- 向子进程提供输入 for i in [0:10000] do grep.stdin.putStrLn (toString i) -- 等待 100ms 让 grep 处理数据，然后读取其输出。 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.
🔗结构体
IO.Process.SpawnArgs : Type
IO.Process.SpawnArgs : Type

将要生成的子进程的配置。

使用 IO.Process.spawn 启动子进程。当子进程应运行至完成，并捕获其输出和/或错误码时，可使用 IO.Process.output 与 IO.Process.run。

构造子

IO.Process.SpawnArgs.mk

扩展

字段

stdin : IO.Process.Stdio

继承自父结构。

stdout : IO.Process.Stdio

继承自父结构。

stderr : IO.Process.Stdio

继承自父结构。

cmd : String

命令名。

args : Array String

命令的实参。

cwd : Option System.FilePath

子进程的工作目录。若为 none，则继承父进程当前工作目录。

env : Array (String × Option String)

为子进程添加或移除环境变量。

子进程会继承父进程的环境，并按 env 中的修改进行调整。数组中的键是环境变量名。none 会从环境中移除该项，some 则将变量设为新值；如有需要会新增该变量。变量按从左到右的顺序处理。

inheritEnv : Bool

从创建它的进程继承环境变量。

setsid : Bool

使用 setsid 在新会话与新进程组中启动子进程。目前在非 POSIX 平台上无效果。

🔗结构体
IO.Process.StdioConfig : Type
IO.Process.StdioConfig : Type

子进程的标准输入、输出与错误句柄的配置。

构造子

IO.Process.StdioConfig.mk

字段

stdin : IO.Process.Stdio

进程标准输入句柄的配置。

stdout : IO.Process.Stdio

进程标准输出句柄的配置。

stderr : IO.Process.Stdio

进程标准错误句柄的配置。

🔗归纳类型
IO.Process.Stdio : Type
IO.Process.Stdio : Type

子进程的标准输入、输出与错误句柄应连接到管道、继承自父进程，还是为空。

如果该流是管道，则父进程可以用它与子进程通信。

构造子

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

该流应连接到管道。

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

该流应继承自父进程。

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

该流应为空。

🔗定义
IO.Process.Stdio.toHandleType : IO.Process.Stdio → Type
IO.Process.Stdio.toHandleType :
  IO.Process.Stdio → Type

可用于通过子进程的标准输入、输出或错误流与之通信的句柄类型。

对于 IO.Process.Stdio.piped，此类型为 IO.FS.Handle。否则它是 Unit，因为无法进行通信。

🔗结构体
IO.Process.Child (cfg : IO.Process.StdioConfig) : Type
IO.Process.Child
  (cfg : IO.Process.StdioConfig) : Type

使用配置 cfg 生成的子进程。

该配置决定了子进程的标准输入、标准输出和标准错误是 IO.FS.Handle 还是 Unit。

字段

stdin : cfg.stdin.toHandleType

若配置为 IO.Process.Stdio.piped，则为子进程的标准输入句柄；否则为 ()。

stdout : cfg.stdout.toHandleType

若配置为 IO.Process.Stdio.piped，则为子进程的标准输出句柄；否则为 ()。

stderr : cfg.stderr.toHandleType

若配置为 IO.Process.Stdio.piped，则为子进程的标准错误句柄；否则为 ()。

🔗不透明定义
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

阻塞直到子进程退出，并返回其退出码。

🔗不透明定义
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)

检查子进程是否已经退出。若进程尚未退出，则返回 none；否则返回其退出码。

🔗不透明定义
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

使用 SIGTERM 信号或平台上的对应机制终止子进程。

如果该进程是使用 SpawnArgs.setsid 启动的，则会改为终止整个进程组。

🔗不透明定义
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 })

从 Child 对象中取出 stdin 字段，从而在保留对子进程引用的同时允许关闭该句柄。

文件句柄会在其最后一个引用被丢弃时关闭。关闭子进程的标准输入会导致一个文件结束标记。由于 Child 对象持有对标准输入的引用，因此若要在进程运行期间关闭该流，就必须执行此操作（例如在调用 Child.wait 后提取其退出码）。许多进程在其标准输入耗尽之前都不会终止。

关闭子进程的标准输入

该程序使用 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 -- 向子进程提供输入 for i in [0:10000] do stdin.putStrLn (toString i) -- 返回不含标准输入句柄的子进程。 -- 这会关闭句柄，因为已不再有 -- 指向它的引用。 pure child -- 等待 grep 终止 if (← grep.wait) != 0 then IO.eprintln s!"grep terminated unsuccessfully" return 1 -- 读取其输出 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.
🔗结构体
IO.Process.Output : Type
IO.Process.Output : Type

进程运行至完成后的结果。

构造子

IO.Process.Output.mk

字段

exitCode : UInt32

进程的退出码。

stdout : String

进程写入其标准输出的全部内容。

stderr : String

进程写入其标准错误的全部内容。