Generated code

A build publishes the module <name> into <out_dir>/<name>, by default $OUT_DIR/lungo/<name>, where <name> is the Lake package’s name unless configured (see configuration). The directory is replaced atomically: it holds either the previous complete output or the new one.

Files

Paths recorded in these files are relative to the Cargo package; files outside it are written <lean>/… (toolchain sources) or <package>/… (Lake dependencies). No file except build-info.json records machine-specific paths.

The aggregate module

lungo::include_lean!("<name>") includes the aggregate from the default output directory, where it expands to include!(concat!(env!("OUT_DIR"), "/lungo/<name>/<name>.rs")). It is usually the only item of a Rust module:

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

Every facade function initializes the program’s modules on first use. Its doc comment records the Lean name, type and source location, unless disable_comments selects it. Generated types derive Clone, Debug (unless skip_debug selects them), and PartialEq, Eq and Hash where all their fields implement them, followed by the configured attributes.

Facility operations

The operations of the program’s facilities (@[lungo_operation] externs) are implemented by the Rust functions rust_extern maps them to. The compiled code calls each through a generated adapter, so the function takes and returns facade types: an operation hostLookup (key : @& String) : Option Nat is implemented by fn lookup(key: String) -> Option<lungo::Nat>, and an IO operation returns Result<T, lungo::IoError>. An operation with a pure Lean type must answer the same arguments the same way: Lean may evaluate a call once and keep its value.

Async exports

An export returning Lungo.Async.Program Op α is an async fn whose first parameter is a handler of the async facility over 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>;

The trait is named after the operation type, <Op>Handler, with one method per constructor of Op, taking the constructor’s fields and answering with the type the facility’s Lungo.Async.Interface instance gives it (async fn implements such a method). The function runs the program, awaits the handler for each operation it asks, and resumes the program with the answer. A method’s error abandons the program and the function returns it. Dropping the future before it completes releases the program and everything it holds. The function needs no particular executor.

__meta

DeclarationInfo:

ExportTrust:

ExportAssurance:

lungo::Assurance holds every record of the assurance document, each slice sorted by name: 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 or ClaimStatus::Incomplete —, evidence_axioms, assumptions, package, fingerprint) and roles (Role: name, role, exported), with schema_version and program. claim(name), claims_about(lean_name), facility(name), assumption(name) and specification(name) look records up.

names.json

An array of records, one per public Rust name:

Items come first, in placement order, then constructors and fields.

externs.json

An array, one record per extern declaration in the program:

sources.json

An array of { lean_name, file, start, end }, with start/end as [line, column] or null, for every source-level declaration with compiled code.

manifest.json

What the exports trust is in assurance.json, with their claims and assumptions.

assurance.json

The program’s assurance document, the same file byte for byte in every output lungo generates for the program, whatever the language. The aggregate module embeds its text as __meta::ASSURANCE_JSON and its records as __meta::assurance() (above). Its schema, ordering and fingerprints are in assurance.json.

build-info.json

Versioning

Generated code asserts the runtime ABI it was generated for at compile time (lungo::__runtime::assert_abi::<N>()), so output generated by a different lungo version fails to compile rather than running against an incompatible runtime.