Module process 

Running external Lean/Lake processes and capturing run provenance.

Structs

LeanInvocation

Lean process invocation metadata.

LeanRunOutput

Raw process output from a Lean check.

Functions

capture_provenance

Capture tooling and repository provenance once for a trace run.

run_lean_file

Run Lean against one file and return a normalized trace.