Skip to main content

aprender_contracts_cli/commands/
lean_status.rs

1use std::path::Path;
2
3use crate::contract_walk::collect_corpus;
4use provable_contracts::lean_gen::{format_status_report, lean_status};
5
6pub fn run(path: &Path) -> Result<(), Box<dyn std::error::Error>> {
7    // PVL-1 (PMAT-1099): an empty corpus is refused (exit 2). A directory report
8    // lists only contracts that carry Lean metadata; a single file is always shown.
9    let is_dir = path.is_dir();
10    let mut contracts = collect_corpus(path)?;
11    contracts.sort_by(|a, b| a.0.cmp(&b.0));
12    let reports: Vec<_> = contracts
13        .into_iter()
14        .map(|(_, c)| lean_status(&c))
15        .filter(|r| !is_dir || r.with_lean > 0)
16        .collect();
17
18    if reports.is_empty() {
19        println!("No Lean proof metadata found in any contracts.");
20    } else {
21        print!("{}", format_status_report(&reports));
22    }
23
24    Ok(())
25}