External process helpers

TorchLean frequently calls out to external tools (Python, Julia, ...), typically in the “untrusted producer, trusted checker” pattern:

• the external tool produces an artifact (often JSON),
• Lean parses it and checks it against a small trusted kernel.

This file centralizes utilities shared across wrappers:

• environment-variable overrides for selecting the executable, and
• availability checks with consistent optional-dependency error messages, and
• “run and parse stdout as JSON” helpers with good error messages.

It intentionally does not provide any claims of correctness about the external tool. It only keeps subprocess handling consistent and non-duplicated.

Executable resolution

def Runtime.External.Process.resolveCmdFromEnv (envVar defaultCmd : String) : IO String

Resolve an executable command name, allowing an environment-variable override.

Example:

• resolveCmdFromEnv "TORCHLEAN_JULIA" "julia" uses $TORCHLEAN_JULIA if set, otherwise "julia".

Availability checks

def Runtime.External.Process.isCmdAvailable (cmd : String) (args : Array String := #["--version"]) : IO Bool

Check whether a command is available by running it with lightweight version-style arguments.

Any exception (including “executable not found”) is treated as false. This helper is for optional dependencies; callers that require the command should use ensureCmdAvailable so users get a helpful message.

def Runtime.External.Process.ensureCmdAvailable (toolName cmd : String) (args : Array String := #["--version"]) (envVar : Option String := none) : IO String

Require a command to be available and return the command name/path.

The toolName and envVar fields are only used in error messages. Wrappers such as Julia or Python oracles use this to keep optional-dependency diagnostics consistent across the codebase.

Running a subprocess and parsing JSON

def Runtime.External.Process.runStdoutChecked (ctx cmd : String) (args : Array String) (cwd : Option String := some ".") : IO String

Run a subprocess and return its captured stdout.

On nonzero exit code, raises IO.userError including stderr. Any exception thrown by the process runner (e.g. executable not found) is propagated to the caller.

def Runtime.External.Process.runJsonStdoutChecked (ctx cmd : String) (args : Array String) (cwd : Option String := some ".") : IO Lean.Json

Run a subprocess, treat its stdout as a single JSON payload, and parse it.

On nonzero exit code, raises IO.userError. If JSON parsing fails, raises IO.userError including the raw stdout (which is usually the most helpful debug output).