9.8. プロセス（Processes）

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

9.8.2. プロセスの実行（Running Processes）

Lean から他のプログラムを実行するには主に3つの方法があります：

  1. IO.Process.run は他のプログラムを同期的に実行し、その標準出力を文字列として返します。プロセスが 0 以外のエラーコードで終了した場合、エラーを投げます。

  2. IO.Process.output は空の標準入力で別のプログラムを同期的に実行し、その標準出力・標準エラー・終了コードをキャプチャします。プロセスが失敗して終了してもエラーは投げられません。

  3. IO.Process.spawn は別のプログラムを非同期に開始し、プロセスの標準入力・標準出力・エラーストリームにアクセスするために使用できるデータ構造を返します。

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

Run process to completion and return stdout on success.

プログラムの実行

このプログラムを実行すると、Unix のツール cat を使って自分のソースコードと自分自身を2回連結します。

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 をフィルタとして使って4桁の回文を見つけます。 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.trim.splitOn "\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)
    : IO IO.Process.Output

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

終了コードのチェック

このプログラムを実行すると、まず存在しないファイルに対して cat を呼び出し、その結果のエラーコードを表示します。その後、Unix のツールである cat を使って自分自身のソースコードと自分自身を2回連結します。

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)
非同期なサブプロセス

このプログラムは Unix ユーティリティ grep をフィルタとして使って4桁の回文を見つけます。 0 から 9999 までのすべての数字を grep プロセスに送り、その結果を読み込みます。このコードは grep が十分に高速で、出力パイプが90個の4桁回文をすべて含むのに十分な大きさがある場合においてのみ正しく動作します。

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

これは以下を出力します：

stdoutThere are 90 four-digit palindromes.
🔗structure
IO.Process.SpawnArgs : Type

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

サブプロセスの標準入力を閉じる

このプログラムは Unix ユーティリティ grep をフィルタとして使って4桁の回文を見つけ、サブプロセスが正常に終了するようにします。 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).trim.splitOn "\n" |>.length IO.println s!"There are {count} four-digit palindromes." return 0

これは以下を出力します：

stdoutThere are 90 four-digit palindromes.
🔗structure
IO.Process.Output : Type

Constructor

IO.Process.Output.mk

Fields

exitCode : UInt32
stdout : String
stderr : String