aprender_contracts_cli/commands/
lean.rs

1use std::fs;
2use std::path::Path;
3
4use provable_contracts::lean_gen::generate_lean_files;
5use provable_contracts::schema::parse_contract;
6
7pub fn run(path: &Path, output_dir: Option<&Path>) -> Result<(), Box<dyn std::error::Error>> {
8    let contract = parse_contract(path)?;
9    let files = generate_lean_files(&contract);
10
11    if files.is_empty() {
12        println!(
13            "No Lean metadata found in {}. Add `lean:` blocks to proof obligations.",
14            path.display()
15        );
16        return Ok(());
17    }
18
19    if let Some(dir) = output_dir {
20        for f in &files {
21            let full = dir.join(&f.path);
22            if let Some(parent) = full.parent() {
23                fs::create_dir_all(parent)?;
24            }
25            fs::write(&full, &f.content)?;
26            println!("  {}", full.display());
27        }
28        println!("\nGenerated {} Lean files.", files.len());
29    } else {
30        // No output dir → print to stdout
31        for f in &files {
32            println!("// === {} ===\n", f.path);
33            print!("{}", f.content);
34            println!();
35        }
36    }
37
38    Ok(())
39}
aprender_contracts_cli/commands/lean.rs

aprender_contracts_cli/commands/
lean.rs
