lean_agent_core/
trace.rs

1//! Trace-run orchestration.
2//!
3//! This module owns the per-run pipeline so the CLI stays thin: capture
4//! provenance once, discover files under each root, run Lean over each, filter,
5//! and stream records to a writer.
6
7use crate::{
8    FileStatus, LeanFile, Result, TraceConfig, TraceRecord, TraceWriter, capture_provenance,
9    discover_lean_files, run_lean_file,
10};
11use camino::Utf8PathBuf;
12use tracing::{info, warn};
13
14/// Outcome counts from a single trace run.
15#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
16pub struct TraceSummary {
17    /// Lean files discovered and executed.
18    pub files_run: usize,
19    /// Records actually written (passes can be filtered out).
20    pub records_written: usize,
21    /// Files whose status was not [`FileStatus::Passed`].
22    pub non_passing: usize,
23}
24
25/// Capture provenance, run Lean over every file under `roots`, and stream
26/// records to `writer`.
27///
28/// Files are discovered per root (honoring `config.recursive`), de-duplicated,
29/// and filtered by `config.exclude`. Non-passing files are always written;
30/// passing files are written only when `config.include_passes` is set.
31pub async fn run_trace(
32    config: &TraceConfig,
33    roots: &[Utf8PathBuf],
34    writer: &mut TraceWriter,
35) -> Result<TraceSummary> {
36    let provenance = capture_provenance(&config.lake_root).await;
37    info!(
38        lean_version = provenance.lean_version.as_deref().unwrap_or("unknown"),
39        lake_version = provenance.lake_version.as_deref().unwrap_or("unknown"),
40        git_commit = provenance.git_commit.as_deref().unwrap_or("none"),
41        "captured run provenance"
42    );
43
44    let files = collect_files(config, roots)?;
45    info!(count = files.len(), "discovered Lean files");
46
47    let mut summary = TraceSummary::default();
48    for file in files {
49        info!(%file, "checking file");
50        let trace = run_lean_file(config, &provenance, file).await;
51        let passed = trace.status == FileStatus::Passed;
52        if !passed {
53            summary.non_passing += 1;
54            warn!(file = %trace.file, status = ?trace.status, "file did not pass");
55        }
56        summary.files_run += 1;
57
58        if config.include_passes || !passed || !trace.diagnostics.is_empty() {
59            writer.write_record(&TraceRecord::FileTrace(trace))?;
60            summary.records_written += 1;
61        }
62    }
63
64    writer.flush()?;
65    Ok(summary)
66}
67
68/// Discover, sort, de-duplicate, and exclude-filter the files under `roots`.
69fn collect_files(config: &TraceConfig, roots: &[Utf8PathBuf]) -> Result<Vec<LeanFile>> {
70    let mut files = Vec::new();
71    for root in roots {
72        files.extend(discover_lean_files(root, config.recursive)?);
73    }
74    files.sort();
75    files.dedup();
76    files.retain(|file| !is_excluded(file, &config.exclude));
77    Ok(files)
78}
79
80/// A file is excluded when any pattern is a substring of its path.
81fn is_excluded(file: &LeanFile, exclude: &[String]) -> bool {
82    let path = file.as_path().as_str();
83    exclude
84        .iter()
85        .any(|pattern| path.contains(pattern.as_str()))
86}
87
88#[cfg(test)]
89mod tests {
90    use super::*;
91
92    fn lean(path: &str) -> LeanFile {
93        LeanFile(Utf8PathBuf::from(path))
94    }
95
96    #[test]
97    fn exclude_matches_substring() {
98        let patterns = vec![".lake/".to_owned(), "Generated".to_owned()];
99        assert!(is_excluded(
100            &lean("project/.lake/build/Foo.lean"),
101            &patterns
102        ));
103        assert!(is_excluded(&lean("src/GeneratedThing.lean"), &patterns));
104        assert!(!is_excluded(&lean("src/Real.lean"), &patterns));
105    }
106
107    #[test]
108    fn empty_exclude_keeps_everything() {
109        assert!(!is_excluded(&lean("anything.lean"), &[]));
110    }
111}
lean_agent_core/trace.rs

lean_agent_core/
trace.rs
