asupersync_conformance/
lean_frontier.rs

1//! Deterministic Lean build frontier extraction and error bucketing.
2//!
3//! The extractor parses Lean diagnostics from `lake build` output, normalizes
4//! signatures, buckets errors by root-cause class, and optionally annotates
5//! buckets with gap/bead ownership links from the Track-2 sequencing plan.
6
7use serde::{Deserialize, Serialize};
8use serde_json::Value;
9use std::collections::{BTreeMap, BTreeSet};
10
11/// Stable schema version for frontier extraction artifacts.
12pub const LEAN_FRONTIER_SCHEMA_VERSION: &str = "1.0.0";
13
14#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
15#[serde(rename_all = "lowercase")]
16pub enum LeanDiagnosticSeverity {
17    Error,
18    Warning,
19}
20
21#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
22pub struct LeanFrontierDiagnostic {
23    pub severity: LeanDiagnosticSeverity,
24    pub file_path: String,
25    pub line: u32,
26    pub column: u32,
27    pub error_code: String,
28    pub failure_mode: String,
29    pub signature: String,
30    pub message: String,
31}
32
33#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
34pub struct LeanFrontierBucket {
35    pub bucket_id: String,
36    pub failure_mode: String,
37    pub error_code: String,
38    pub count: usize,
39    pub signatures: Vec<String>,
40    pub sample_locations: Vec<String>,
41    pub linked_gap_ids: Vec<String>,
42    pub linked_bead_ids: Vec<String>,
43}
44
45#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
46pub struct LeanFrontierReport {
47    pub schema_version: String,
48    pub report_id: String,
49    pub generated_by: String,
50    pub source_log: String,
51    pub bucket_ordering: String,
52    pub diagnostics_total: usize,
53    pub errors_total: usize,
54    pub warnings_total: usize,
55    pub buckets: Vec<LeanFrontierBucket>,
56}
57
58#[derive(Debug, Default)]
59struct GapLinks {
60    gap_ids: BTreeSet<String>,
61    bead_ids: BTreeSet<String>,
62}
63
64/// Parse and bucket Lean diagnostics from build output.
65///
66/// The output ordering is deterministic:
67/// - diagnostics are parsed in input order
68/// - buckets are sorted by `(failure_mode, error_code)`
69/// - signatures and locations are sorted lexicographically
70pub fn extract_frontier_report(
71    log_text: &str,
72    source_log: &str,
73    gap_plan_json: Option<&str>,
74) -> LeanFrontierReport {
75    let gap_links = parse_gap_links(gap_plan_json);
76
77    let diagnostics = log_text
78        .lines()
79        .filter_map(parse_diagnostic_line)
80        .collect::<Vec<_>>();
81    let errors_total = diagnostics
82        .iter()
83        .filter(|d| d.severity == LeanDiagnosticSeverity::Error)
84        .count();
85    let warnings_total = diagnostics
86        .iter()
87        .filter(|d| d.severity == LeanDiagnosticSeverity::Warning)
88        .count();
89
90    let mut grouped = BTreeMap::<(String, String), Vec<LeanFrontierDiagnostic>>::new();
91    for diagnostic in diagnostics
92        .iter()
93        .filter(|d| d.severity == LeanDiagnosticSeverity::Error)
94    {
95        grouped
96            .entry((
97                diagnostic.failure_mode.clone(),
98                diagnostic.error_code.clone(),
99            ))
100            .or_default()
101            .push(diagnostic.clone());
102    }
103
104    let mut buckets = Vec::with_capacity(grouped.len());
105    for ((failure_mode, error_code), mut entries) in grouped {
106        entries.sort_by(|left, right| {
107            (
108                left.file_path.as_str(),
109                left.line,
110                left.column,
111                left.signature.as_str(),
112            )
113                .cmp(&(
114                    right.file_path.as_str(),
115                    right.line,
116                    right.column,
117                    right.signature.as_str(),
118                ))
119        });
120
121        let signatures = entries
122            .iter()
123            .map(|entry| entry.signature.clone())
124            .collect::<BTreeSet<_>>()
125            .into_iter()
126            .collect::<Vec<_>>();
127        let sample_locations = entries
128            .iter()
129            .map(|entry| format!("{}:{}:{}", entry.file_path, entry.line, entry.column))
130            .collect::<BTreeSet<_>>()
131            .into_iter()
132            .take(12)
133            .collect::<Vec<_>>();
134        let (linked_gap_ids, linked_bead_ids) = gap_links
135            .get(&failure_mode)
136            .map(|links| {
137                (
138                    links.gap_ids.iter().cloned().collect::<Vec<_>>(),
139                    links.bead_ids.iter().cloned().collect::<Vec<_>>(),
140                )
141            })
142            .unwrap_or_default();
143
144        buckets.push(LeanFrontierBucket {
145            bucket_id: format!("{failure_mode}.{error_code}"),
146            failure_mode,
147            error_code,
148            count: entries.len(),
149            signatures,
150            sample_locations,
151            linked_gap_ids,
152            linked_bead_ids,
153        });
154    }
155
156    LeanFrontierReport {
157        schema_version: LEAN_FRONTIER_SCHEMA_VERSION.to_string(),
158        report_id: "lean.frontier.buckets.v1".to_string(),
159        generated_by: "bd-1dorb".to_string(),
160        source_log: source_log.to_string(),
161        bucket_ordering: "lexicographic(failure_mode,error_code)".to_string(),
162        diagnostics_total: diagnostics.len(),
163        errors_total,
164        warnings_total,
165        buckets,
166    }
167}
168
169fn parse_gap_links(gap_plan_json: Option<&str>) -> BTreeMap<String, GapLinks> {
170    let mut by_failure_mode = BTreeMap::<String, GapLinks>::new();
171    let Some(json) = gap_plan_json else {
172        return by_failure_mode;
173    };
174
175    let Ok(plan) = serde_json::from_str::<Value>(json) else {
176        return by_failure_mode;
177    };
178    let Some(gaps) = plan.get("gaps").and_then(Value::as_array) else {
179        return by_failure_mode;
180    };
181
182    for gap in gaps {
183        let Some(failure_mode) = gap.get("failure_mode").and_then(Value::as_str) else {
184            continue;
185        };
186        let Some(gap_id) = gap.get("id").and_then(Value::as_str) else {
187            continue;
188        };
189        let links = by_failure_mode.entry(failure_mode.to_string()).or_default();
190        links.gap_ids.insert(gap_id.to_string());
191        if let Some(linked_beads) = gap.get("linked_beads").and_then(Value::as_array) {
192            for bead in linked_beads.iter().filter_map(Value::as_str) {
193                links.bead_ids.insert(bead.to_string());
194            }
195        }
196    }
197
198    by_failure_mode
199}
200
201fn parse_diagnostic_line(line: &str) -> Option<LeanFrontierDiagnostic> {
202    let (severity, rest) = if let Some(rest) = line.strip_prefix("error: ") {
203        (LeanDiagnosticSeverity::Error, rest)
204    } else {
205        let rest = line.strip_prefix("warning: ")?;
206        (LeanDiagnosticSeverity::Warning, rest)
207    };
208
209    let mut parts = rest.splitn(4, ':');
210    let raw_file = parts.next()?.trim();
211    let line_number = parts.next()?.trim().parse::<u32>().ok()?;
212    let column = parts.next()?.trim().parse::<u32>().ok()?;
213    let message = parts.next()?.trim().to_string();
214    if raw_file.is_empty() || message.is_empty() {
215        return None;
216    }
217
218    let file_path = normalize_file_path(raw_file);
219    let error_code = classify_error_code(&message).to_string();
220    let failure_mode = classify_failure_mode(&error_code).to_string();
221    let signature = format!(
222        "{file_path}:{error_code}:{}",
223        normalize_message_for_signature(&message)
224    );
225
226    Some(LeanFrontierDiagnostic {
227        severity,
228        file_path,
229        line: line_number,
230        column,
231        error_code,
232        failure_mode,
233        signature,
234        message,
235    })
236}
237
238fn normalize_file_path(raw_file: &str) -> String {
239    raw_file.rsplit('/').next().unwrap_or(raw_file).to_string()
240}
241
242fn classify_error_code(message: &str) -> &'static str {
243    let lower = message.to_ascii_lowercase();
244    if lower.starts_with("unknown identifier") {
245        return "unknown-identifier";
246    }
247    if lower.starts_with("alternative `") && lower.contains("has not been provided") {
248        return "constructor-alternative-missing";
249    }
250    if lower.contains("maximum recursion depth has been reached") {
251        return "tactic-max-rec-depth";
252    }
253    if lower.contains("tactic `simp` failed with a nested error") {
254        return "tactic-simp-nested-error";
255    }
256    if lower.contains("unsolved goals") {
257        return "unsolved-goals";
258    }
259    if lower.starts_with("application type mismatch") {
260        return "application-type-mismatch";
261    }
262    if lower.starts_with("type mismatch") {
263        return "type-mismatch";
264    }
265    if lower.contains("tactic `rewrite` failed") {
266        return "rewrite-failed";
267    }
268    if lower.contains("tactic `subst` failed") {
269        return "subst-failed";
270    }
271    if lower.contains("no goals to be solved") {
272        return "no-goals";
273    }
274    if lower.contains("unexpected token") {
275        return "parse-unexpected-token";
276    }
277    if lower.contains("omega could not prove the goal") {
278        return "omega-goal-not-proved";
279    }
280    if lower.contains("simp made no progress") {
281        return "simp-no-progress";
282    }
283    "other"
284}
285
286fn classify_failure_mode(error_code: &str) -> &'static str {
287    match error_code {
288        "unknown-identifier" => "declaration-order",
289        "constructor-alternative-missing" => "missing-lemma",
290        "tactic-max-rec-depth" | "tactic-simp-nested-error" | "simp-no-progress" => {
291            "tactic-instability"
292        }
293        "application-type-mismatch"
294        | "type-mismatch"
295        | "rewrite-failed"
296        | "subst-failed"
297        | "unsolved-goals"
298        | "no-goals"
299        | "parse-unexpected-token"
300        | "omega-goal-not-proved"
301        | "other" => "proof-shape",
302        _ => "proof-shape",
303    }
304}
305
306fn normalize_message_for_signature(message: &str) -> String {
307    let mut out = String::with_capacity(message.len());
308    let mut in_backticks = false;
309    let mut digit_run = false;
310    let mut previous_was_space = false;
311
312    for ch in message.chars() {
313        if ch == '`' {
314            if in_backticks {
315                if !out.ends_with("<id>") {
316                    out.push_str("<id>");
317                }
318                previous_was_space = false;
319            }
320            in_backticks = !in_backticks;
321            continue;
322        }
323        if in_backticks {
324            continue;
325        }
326        if ch.is_ascii_digit() {
327            if !digit_run {
328                out.push('#');
329                digit_run = true;
330                previous_was_space = false;
331            }
332            continue;
333        }
334        digit_run = false;
335        let lowered = ch.to_ascii_lowercase();
336        if lowered.is_ascii_alphanumeric() || lowered == '-' || lowered == '_' {
337            out.push(lowered);
338            previous_was_space = false;
339            continue;
340        }
341        if !previous_was_space {
342            out.push(' ');
343            previous_was_space = true;
344        }
345    }
346
347    out.split_whitespace().collect::<Vec<_>>().join(" ")
348}
349
350#[cfg(test)]
351mod tests {
352    use super::{
353        LEAN_FRONTIER_SCHEMA_VERSION, LeanDiagnosticSeverity, extract_frontier_report,
354        normalize_message_for_signature, parse_diagnostic_line,
355    };
356
357    #[test]
358    fn parse_diagnostic_line_extracts_expected_fields() {
359        let line = "error: Asupersync.lean:2874:2: Alternative `cancelChild` has not been provided";
360        let diagnostic = parse_diagnostic_line(line).expect("must parse");
361        assert_eq!(diagnostic.severity, LeanDiagnosticSeverity::Error);
362        assert_eq!(diagnostic.file_path, "Asupersync.lean");
363        assert_eq!(diagnostic.line, 2874);
364        assert_eq!(diagnostic.column, 2);
365        assert_eq!(diagnostic.error_code, "constructor-alternative-missing");
366        assert_eq!(diagnostic.failure_mode, "missing-lemma");
367    }
368
369    #[test]
370    fn signature_normalization_stabilizes_identifiers_and_numbers() {
371        let message = "Unknown identifier `setRegion_structural_preserves_wellformed` at 2335";
372        let normalized = normalize_message_for_signature(message);
373        assert_eq!(normalized, "unknown identifier <id> at #");
374    }
375
376    #[test]
377    fn extraction_is_deterministic_for_same_input() {
378        let log = "\
379error: Asupersync.lean:10:2: Unknown identifier `x`\n\
380error: Asupersync.lean:11:2: Unknown identifier `y`\n\
381error: Asupersync.lean:12:3: Type mismatch\n\
382warning: Asupersync.lean:13:5: unused variable `h`\n\
383";
384        let report_a = extract_frontier_report(log, "sample.log", None);
385        let report_b = extract_frontier_report(log, "sample.log", None);
386        assert_eq!(report_a, report_b);
387        assert_eq!(report_a.schema_version, LEAN_FRONTIER_SCHEMA_VERSION);
388        assert_eq!(report_a.diagnostics_total, 4);
389        assert_eq!(report_a.errors_total, 3);
390        assert_eq!(report_a.warnings_total, 1);
391    }
392}
asupersync_conformance/lean_frontier.rs

asupersync_conformance/
lean_frontier.rs
