Julia subprocess integration (optional)

This module provides a small wrapper around IO.Process for calling out to Julia.

Why this exists:

• TorchLean sometimes treats external tools as untrusted producers (e.g. Julia doing a heavy numeric search on CPU/GPU) and then checks a small certificate artifact in Lean.
• The IO boundary is explicit: any result returned by Julia should be treated as untrusted unless validated in Lean.

This mirrors the existing patterns used in TorchLean for:

• Arb via Python (NN/Floats/Arb/Oracle.lean), and
• Gymnasium via Python (NN/Runtime/RL/Gymnasium/Client.lean).

Optional dependency:

• This file compiles without Julia installed.
• Julia is only required if you execute code that calls run/runJson.
• You can override the Julia executable path via the TORCHLEAN_JULIA environment variable.

References:

• Lean IO.Process: https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html
• Julia language: https://julialang.org/

Resolving the Julia executable

def Runtime.External.Julia.resolveJuliaCmd (juliaCmd : String := "julia") : IO String

Resolve which Julia executable to use.

If the environment variable TORCHLEAN_JULIA is set, it takes precedence. Otherwise we fall back to juliaCmd (default: "julia"), which is expected to be on PATH.

Availability checks

def Runtime.External.Julia.ensureAvailable (juliaCmd : String := "julia") : IO String

Require Julia to be available and return the resolved command.

This is suitable for example runners that want a friendly error message when Julia is missing.

Running Julia

def Runtime.External.Julia.run (args : Array String) (cwd : Option String := some ".") (juliaCmd : String := "julia") : IO String

Run Julia with the given CLI arguments and return stdout.

On nonzero exit code, we raise IO.userError including the captured stderr. The cwd defaults to "." so relative script paths behave like in other TorchLean subprocess integrations.

def Runtime.External.Julia.runJson (args : Array String) (cwd : Option String := some ".") (juliaCmd : String := "julia") : IO Lean.Json

Run Julia and parse stdout as JSON.

Certificate producer scripts commonly print one JSON payload to stdout; this entrypoint checks the Julia process and parses that payload.