Skip to main content

aprender_contracts_cli/commands/
lean_status.rs

1use std::path::Path;
2
3use provable_contracts::lean_gen::{format_status_report, lean_status};
4use provable_contracts::schema::parse_contract;
5
6use crate::contract_walk::collect_contracts;
7
8pub fn run(path: &Path) -> Result<(), Box<dyn std::error::Error>> {
9    let reports = if path.is_dir() {
10        let mut contracts = Vec::new();
11        collect_contracts(path, &mut contracts);
12        contracts.sort_by(|a, b| a.0.cmp(&b.0));
13        contracts
14            .into_iter()
15            .map(|(_, c)| lean_status(&c))
16            .filter(|r| r.with_lean > 0)
17            .collect()
18    } else {
19        let contract = parse_contract(path)?;
20        vec![lean_status(&contract)]
21    };
22
23    if reports.is_empty() {
24        println!("No Lean proof metadata found in any contracts.");
25    } else {
26        print!("{}", format_status_report(&reports));
27    }
28
29    Ok(())
30}