Come eseguire il main di un programma Lean da Rust

Questa guida mostra come compilare un eseguibile Lean, cioè uno con un main, come binario Rust.

Genera il programma

Il modulo che definisce main deve essere un modulo radice. Un eseguibile Lake che è un target predefinito rende già radice il suo root, quindi una build dei target predefiniti del pacchetto non richiede configurazione. main può avere una qualsiasi delle forme di Lean: IO Unit, IO UInt32, List String → IO Unit oppure List String → IO UInt32.

// build.rs
fn main() -> lungo_build::Result<()> {
    lungo_build::configure().root_module("Tool.Main").name("program").compile_lean("lean")
}

Il modulo generato ha allora __lean_main() e __lean_main_with(args).

Chiamalo

// src/main.rs
mod program {
    lungo::include_lean!("program");
}

fn main() {
    std::process::exit(program::__lean_main());
}

__lean_main() passa gli argomenti del processo (senza il nome del programma) al main di Lean, lo esegue su un thread con la dimensione di stack che i programmi Lean si aspettano e restituisce il codice di uscita: l’UInt32 restituito da Lean, 0 per Unit, oppure 1 dopo aver stampato un errore IO non gestito come fa Lean (uncaught exception: …).

Per passare altri argomenti, chiama program::__lean_main_with(vec!["--flag".into()]).

Più programmi in un solo binario

Dai a ogni programma un nome proprio:

// build.rs
fn main() -> lungo_build::Result<()> {
    for (name, root) in [("fmt", "Tool.Fmt"), ("check", "Tool.Check")] {
        lungo_build::configure().root_module(root).name(name).compile_lean("lean")?;
    }
    Ok(())
}

e scegli in base a esso:

// src/main.rs
mod fmt {
    lungo::include_lean!("fmt");
}
mod check {
    lungo::include_lean!("check");
}

fn main() {
    let mut args = std::env::args().skip(1);
    let code = match args.next().as_deref() {
        Some("fmt") => fmt::__lean_main_with(args.collect()),
        Some("check") => check::__lean_main_with(args.collect()),
        _ => 2,
    };
    std::process::exit(code);
}

compiler-tests/runner in lungo-rs genera in questo modo ogni eseguibile di un progetto Lake.