Come confrontare il Rust generato con il backend nativo di Lean

Questa guida mostra come compilare lo stesso progetto Lean sia come Rust generato (PureRust) sia sul backend nativo di Lean (LeanOracle) nello stesso crate, e come verificare che entrambi diano gli stessi risultati. Usala per testare la traduzione in Rust del tuo codice Lean.

LeanOracle compila solo per l’host e, su Windows, richiede un target Rust *-windows-gnu (vedi piattaforme).

Genera entrambe le modalità

Dai a ciascuna modalità un nome proprio in build.rs:

use lungo_build::Mode;

fn main() -> lungo_build::Result<()> {
    for (name, mode) in [("pure", Mode::PureRust), ("oracle", Mode::LeanOracle)] {
        lungo_build::configure().mode(mode).name(name).compile_lean("lean")?;
    }
    Ok(())
}

e includi ciascuna come modulo a sé:

pub mod pure {
    lungo::include_lean!("pure");
}

pub mod oracle {
    lungo::include_lean!("oracle");
}

LeanOracle compila il codice C del progetto con il leanc della toolchain e collega il runtime di Lean; lo script di build stampa le direttive di collegamento.

Confronta i risultati

Entrambi i moduli hanno le stesse funzioni e tipi strutturalmente identici. I tipi dichiarati dal progetto Lean sono tipi Rust distinti in ciascun modulo, quindi costruisci gli input separatamente per ciascuno e confronta i risultati attraverso una forma comune, come la loro resa Debug:

use lungo::Nat;

#[test]
fn both_backends_agree() {
    for (a, b) in [(0u64, 0u64), (7, 3), (u64::MAX, 2)] {
        let p = pure::nat_ops(Nat::from(a), Nat::from(b));
        let o = oracle::nat_ops(Nat::from(a), Nat::from(b));
        assert_eq!(format!("{p:?}"), format!("{o:?}"));
    }
}

L’output Debug dei float è esatto (distingue -0.0 e NaN), quindi confronta fedelmente i risultati in virgola mobile.

Per una copertura ampia, genera gli input con una libreria di property testing come proptest. compiler-tests/facade-runner in lungo-rs confronta in questo modo ogni funzione di una libreria Lean.