Skip to main content

parse_lean_diagnostics

lean_agent_core::diagnostics

Function parse_lean_diagnostics 

Source 
pub fn parse_lean_diagnostics(
    output: &str,
    include_warnings: bool,
) -> Vec<Diagnostic>
Expand description

Parse Lean diagnostics from stderr/stdout text.

TODO(parser-hardening): Replace this first-pass regex parser with a snapshot-tested parser over a corpus of Lean 4 diagnostic fixtures from mathlib and your own repos.