aprender-contracts-cli 0.32.0

CLI for provable-contracts — validate, scaffold, verify, status, audit
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39

use std::fs;
use std::path::Path;

use provable_contracts::lean_gen::generate_lean_files;
use provable_contracts::schema::parse_contract;

pub fn run(path: &Path, output_dir: Option<&Path>) -> Result<(), Box<dyn std::error::Error>> {
    let contract = parse_contract(path)?;
    let files = generate_lean_files(&contract);

    if files.is_empty() {
        println!(
            "No Lean metadata found in {}. Add `lean:` blocks to proof obligations.",
            path.display()
        );
        return Ok(());
    }

    if let Some(dir) = output_dir {
        for f in &files {
            let full = dir.join(&f.path);
            if let Some(parent) = full.parent() {
                fs::create_dir_all(parent)?;
            }
            fs::write(&full, &f.content)?;
            println!("  {}", full.display());
        }
        println!("\nGenerated {} Lean files.", files.len());
    } else {
        // No output dir → print to stdout
        for f in &files {
            println!("// === {} ===\n", f.path);
            print!("{}", f.content);
            println!();
        }
    }

    Ok(())
}