lean_agent_core/
diagnostics.rs

1//! Parsing Lean/Lake diagnostic output.
2//!
3//! This starts intentionally conservative. The parser should preserve raw messages and only
4//! structure fields it can infer reliably.
5
6use crate::{Diagnostic, DiagnosticSeverity, GoalState};
7use camino::Utf8PathBuf;
8use regex::Regex;
9
10/// Parse Lean diagnostics from stderr/stdout text.
11///
12/// TODO(parser-hardening): Replace this first-pass regex parser with a snapshot-tested parser
13/// over a corpus of Lean 4 diagnostic fixtures from mathlib and your own repos.
14#[must_use]
15pub fn parse_lean_diagnostics(output: &str, include_warnings: bool) -> Vec<Diagnostic> {
16    let Ok(header) = Regex::new(
17        r"(?m)^(?P<file>[^:\n]+\.lean):(?P<line>\d+):(?P<column>\d+):\s*(?P<severity>error|warning|information):\s*(?P<message>.*)$",
18    ) else {
19        return Vec::new();
20    };
21
22    let mut diagnostics = Vec::new();
23    let mut matches = header.captures_iter(output).peekable();
24
25    while let Some(caps) = matches.next() {
26        let Some(full_match) = caps.get(0) else {
27            continue;
28        };
29        let message_start = full_match.start();
30        let next_start = matches
31            .peek()
32            .and_then(|next| next.get(0))
33            .map_or(output.len(), |m| m.start());
34        let block = output[message_start..next_start].trim();
35
36        let severity = match &caps["severity"] {
37            "error" => DiagnosticSeverity::Error,
38            "warning" => DiagnosticSeverity::Warning,
39            "information" => DiagnosticSeverity::Info,
40            _ => DiagnosticSeverity::Unknown,
41        };
42
43        if severity == DiagnosticSeverity::Warning && !include_warnings {
44            continue;
45        }
46
47        let file = Some(Utf8PathBuf::from(&caps["file"]));
48        let line = caps["line"].parse::<u32>().ok();
49        let column = caps["column"].parse::<u32>().ok();
50        let message = block.to_owned();
51        let goal_state = extract_goal_state(block);
52
53        diagnostics.push(Diagnostic {
54            file,
55            line,
56            column,
57            severity,
58            message,
59            goal_state,
60        });
61    }
62
63    diagnostics
64}
65
66fn extract_goal_state(block: &str) -> Option<GoalState> {
67    // TODO(goal-parser): Lean goal output has multiple shapes. Expand this with real fixtures.
68    let marker = "unsolved goals";
69    let idx = block.find(marker)?;
70    let rest = block[idx + marker.len()..].trim();
71    if rest.is_empty() {
72        None
73    } else {
74        Some(GoalState(rest.to_owned()))
75    }
76}
77
78#[cfg(test)]
79mod tests {
80    use super::*;
81
82    #[test]
83    fn parses_basic_unsolved_goal() {
84        let raw = include_str!("../tests/fixtures/unsolved_goal.stderr");
85        let diagnostics = parse_lean_diagnostics(raw, true);
86        assert_eq!(diagnostics.len(), 1);
87        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Error);
88        assert!(diagnostics[0].goal_state.is_some());
89    }
90}
lean_agent_core/diagnostics.rs

lean_agent_core/
diagnostics.rs
