Lean 4 (Meta)programming Cookbook

Running an external program🔗

Contributors: Anirudh Gupta

In order to run an external program from inside a Lean file, we can use IO.Process.run, which takes a IO.Process.SpawnArgs structure and returns the command's stdout as a String.

def runExternalProgram (cmd : String) (args : Array String) : IO String := IO.Process.run { cmd := cmd args := args } -- #eval runExternalProgram "curl" #["https://www.test.com"]

If the program fails (returns a non-zero exit code), IO.Process.run will throw an exception. To handle the output more gracefully and see the exit code and stderr, you can use IO.Process.output.

def runExternalWithOutput (cmd : String) (args : Array String) : IO Unit := do let out IO.Process.output { cmd := cmd args := args } if out.exitCode == 0 then IO.println s!"Command succeeded: {out.stdout}" else IO.println s!"Command failed. Exit Code: {out.exitCode}, Error: {out.stderr}"

If you want to know more information about the process, such as its PID, you can use IO.Process.spawn to start the process and get a IO.Process object.

def spawnExternalProgram (cmd : String) (args : Array String) : IO Unit := do let proc IO.Process.spawn { cmd := cmd args := args } IO.println s!"Spawned process with PID: {proc.pid}" let exitCode proc.wait IO.println s!"Process exited with code: {exitCode}" -- #eval spawnExternalProgram "touch" #["test.txt"]
  1. Application: File Compression and Decompression