Codice generato

Una build pubblica il modulo <name> in <out_dir>/<name>, per impostazione predefinita $OUT_DIR/lungo/<name>, dove <name> è il nome del pacchetto Lake salvo diversa configurazione (vedi configurazione). La directory viene sostituita in modo atomico: contiene o l’output completo precedente o quello nuovo.

File

I percorsi registrati in questi file sono relativi al pacchetto Cargo; i file al di fuori sono scritti <lean>/… (sorgenti della toolchain) o <package>/… (dipendenze Lake). Nessun file tranne build-info.json registra percorsi specifici della macchina.

Il modulo aggregato

lungo::include_lean!("<name>") include l’aggregato dalla directory di output predefinita, dove si espande in include!(concat!(env!("OUT_DIR"), "/lungo/<name>/<name>.rs")). Di solito è l’unico elemento di un modulo Rust:

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

Ogni funzione della facciata inizializza i moduli del programma al primo uso. Il suo commento di documentazione registra il nome Lean, il tipo e la posizione nel sorgente, a meno che disable_comments la selezioni. I tipi generati derivano Clone, Debug (a meno che skip_debug li selezioni), e PartialEq, Eq e Hash dove tutti i loro campi li implementano, seguiti dagli attributi configurati.

Operazioni delle facility

Le operazioni delle facility del programma (gli extern @[lungo_operation]) sono implementate dalle funzioni Rust su cui le mappa rust_extern. Il codice compilato chiama ciascuna tramite un adattatore generato, quindi la funzione prende e restituisce tipi di facciata: un’operazione hostLookup (key : @& String) : Option Nat è implementata da fn lookup(key: String) -> Option<lungo::Nat>, e un’operazione IO restituisce Result<T, lungo::IoError>. Un’operazione con un tipo Lean puro deve rispondere allo stesso modo agli stessi argomenti: Lean può valutare una chiamata una sola volta e conservarne il valore.

Export asincroni

Un export che restituisce Lungo.Async.Program Op α è una async fn il cui primo parametro è un handler della facility asincrona su Op:

pub trait AskHandler {
    /// What a method fails with.
    type Error;
    /// Performs `Host.Ask.fetch`.
    fn fetch(&self, key: String) -> impl Future<Output = Result<Result<Nat, String>, Self::Error>>;
    /// Performs `Host.Ask.tool`.
    fn tool(&self, name: String) -> impl Future<Output = Result<LeanClosure<fn(Nat) -> Nat>, Self::Error>>;
}

pub async fn sum_keys<H: AskHandler>(handler: &H, keys: List<String>) -> Result<Nat, H::Error>;

Il tratto prende il nome dal tipo di operazioni, <Op>Handler, con un metodo per ogni costruttore di Op, che prende i campi del costruttore e risponde con il tipo che gli assegna l’istanza Lungo.Async.Interface della facility (una async fn implementa un tale metodo). La funzione esegue il programma, attende l’handler per ogni operazione che chiede e riprende il programma con la risposta. Un errore di un metodo abbandona il programma e la funzione lo restituisce. Abbandonare il future prima che termini rilascia il programma e tutto ciò che trattiene. La funzione non richiede un executor particolare.

__meta

DeclarationInfo:

ExportTrust:

ExportAssurance:

lungo::Assurance contiene ogni record del documento di garanzia, ogni slice ordinata per nome: specifications (Specification: name, kind, statement, definition, package, fingerprint), facilities (Facility: name, id, asynchronous, operations, assumptions, package, fingerprint), assumptions (Assumption: name, facility, statement, definition, package, fingerprint), claims (Claim: name, relation, subjects, specifications, statement, status — ClaimStatus::Proved o ClaimStatus::Incomplete —, evidence_axioms, assumptions, package, fingerprint) e roles (Role: name, role, exported), con schema_version e program. claim(name), claims_about(lean_name), facility(name), assumption(name) e specification(name) cercano i record.

names.json

Un array di record, uno per ogni nome Rust pubblico:

Prima vengono gli elementi, in ordine di collocazione, poi i costruttori e i campi.

externs.json

Un array, un record per ogni dichiarazione extern del programma:

sources.json

Un array di { lean_name, file, start, end }, con start/end come [line, column] oppure null, per ogni dichiarazione a livello di sorgente con codice compilato.

manifest.json

Ciò di cui gli export si fidano sta in assurance.json, con i loro claim e le loro assunzioni.

assurance.json

Il documento di garanzia del programma, lo stesso file byte per byte in ogni output che lungo genera per il programma, qualunque sia il linguaggio. Il modulo aggregato ne incorpora il testo come __meta::ASSURANCE_JSON e i record come __meta::assurance() (sopra). Il suo schema, l’ordinamento e i fingerprint sono in assurance.json.

build-info.json

Versionamento

Il codice generato verifica in fase di compilazione l’ABI del runtime per cui è stato generato (lungo::__runtime::assert_abi::<N>()), così un output generato da una versione diversa di lungo non compila invece di essere eseguito con un runtime incompatibile.