Skip to main content

run_lean_file

lean_agent_core::process

Function run_lean_file 

Source 
pub async fn run_lean_file(
    config: &TraceConfig,
    provenance: &Provenance,
    file: LeanFile,
) -> FileTrace
Expand description

Run Lean against one file and return a normalized trace.

This never fails: a timeout becomes a FileStatus::TimedOut record and a spawn/wait failure becomes a FileStatus::RunnerError record, each carrying the run provenance so every record stays self-describing.