Configuration

lungo is configured in two places that describe the same settings:

• lungo.toml, read by the lungo command, for every output language;
• a lungo_build::Builder in a Cargo build.rs, for the Rust output (compile_lean(project) is configure().compile_lean(project)).

Every setting has a default. Unknown keys are errors (LNG0107).

# lungo.toml
project = "lean"

[lean]
root-modules = ["Formal.Session"]
assurance-modules = ["Formal.Laws"]

[assurance]
require-claims = ["Formal.Session"]

[rust]
out-dir = "src/generated"
type-attributes = [
  { path = "Formal", attribute = "#[derive(serde::Serialize, serde::Deserialize)]" },
]
rust-externs = { host_log = "crate::host::log" }

[go]
out = "gen/formal"
options = { package = "formal" }

[plugins.kotlin]
out = "gen/kotlin"

// build.rs
fn main() -> lungo_build::Result<()> {
    lungo_build::configure()
        .root_module("Formal.Session")
        .assurance_module("Formal.Laws")
        .require_claims("Formal.Session")
        .type_attribute("Formal", "#[derive(serde::Serialize, serde::Deserialize)]")
        .rust_extern("host_log", "crate::host::log")
        .compile_lean("lean")
}

The file

Paths in the file (project, out, out-dir, toolchain-dir) are relative to the file’s directory. lungo keeps scratch files in .lungo/ next to the file; add it to .gitignore.

Program

Set in [lean], or with the Builder methods:

Which externs the host implements is not a setting: the program’s Lean code declares them, as the operations of facilities (@[lungo_facility] and @[lungo_operation]; see how to call host code from Lean). Every generated package asks the host for every operation of every facility the program’s linked modules declare. An operation’s extern key is the symbol of its @[extern "symbol"], or the declaration’s name for the other extern forms.

Without root_module, the roots are what lake build builds: the root modules of every default target of the root package (defaultTargets in lakefile.toml, @[default_target] in lakefile.lean), which are Lean libraries (their roots) or Lean executables (their root). A package without default targets needs root_module (LNG0301).

Without export and export_module, the root modules and their submodules are exported. From an exported module, definitions are exported unless they are private, internal (_-prefixed components), instances or their methods, compiler-generated (recursors, matchers, noConfusion, projections, constructors, structural auxiliaries), syntax node kinds (syntax, notation, macro), or meta definitions.

Trust policy

Set in [lean]:

deny_sorry and deny_axioms also apply to the evidence of every claim (the theorem it names): a claim proved with sorry, or with an axiom the policy denies, is refused as an export would be. With deny-sorry = false, such a claim is reported with status incomplete, and is not a proved claim for require-claims.

Violations fail the build with LNG0601.

Assurance policy

Set in [assurance], or with the Builder methods. lungo first checks the program’s assurance records themselves (their form, the declarations they name, the shape of each claim); a problem with one fails the build whatever the policy, with its own code (LNG0701–LNG0710). Then:

A path that selects no export, or a name that is neither an assumption nor a facility of the program, is an error (LNG0107): it cannot have any effect.

The policy is part of what an output is generated from: tightening it makes lungo generate check an output again rather than keep it as up to date.

Worker

Set in [lean]:

Toolchain

Set in [lean]:

Rust

Set in [rust], or with the Builder methods:

One build script may compile several Lean projects; each generates its own module, and two that would generate the same module are an error (LNG0107). Give one of them another name.

Shaping the generated code

These settings select generated items by path. The path . selects every item; any other path selects the Lean name it spells and every name in it as a namespace: Formal selects Formal.Sess and Formal.Sess.isOpen, but Formal.Se selects neither. Fields are named as in names.json: <Structure>.<field>, <Constructor>.<binder>, or <Constructor>#<index>. A path other than . that selects nothing is an error (LNG0107): it cannot have any effect.

In TOML, attribute settings are lists of { path, attribute } tables, skip-debug and disable-comments lists of paths, and extern-types a table from Lean type to Rust path.

Attributes are written as in Rust source, #[…], and are placed after the derives lungo generates (Clone, Debug, and PartialEq, Eq, Hash where every field has them), so they may be #[derive(…)]s of further traits or attributes of those derives, such as #[serde(…)]. The serde feature of the lungo crate implements serde for the facade types.

An extern type implements lungo::LeanType for the backend in use, has the Lean type’s parameters, and represents its values as the Lean type does; in practice it is the type another lungo build generated for the same Lean type. It is not generated, and types containing it derive only Clone and Debug. It also implements lungo::LeanLayout with the Lean type’s layout fingerprint, which the generated module checks when it is compiled (see extern types); a type generated by lungo implements it already. See How to share types between Lean projects.

Generator options

A language’s table holds its output directory, out, and its options, options, a table of strings. --<language>_opt=KEY=VALUE on the command line adds to (and overrides) them. A generator rejects options it does not know.

Go is always a package of the host’s module; it has no embed. See generated packages for what each generator writes.

Extern types

A program built on another program’s model (a Lake package requiring another) uses that program’s types. Generated separately, each package would have its own type for them, and a value of one could not be passed to the other. A language’s extern-types table names, for a Lean type, the other generated package’s type to use instead:

[go.extern-types."TaggedUrn.Exec.Wf"]
package = "github.com/machinefabric/tagged-urn-go/formal"   # what an import names
name = "Wf"                                                 # the type, as that generator named it

The type must be one the program’s functions or facility operations use (LNG0107 otherwise). Values then pass between the two packages as they are: data by value, and values held by handle as the same handle, since every package of a process runs on the one runtime.

In TypeScript each program runs in a WebAssembly instance of its own, with a handle table of its own, so only types whose values are data can be extern types; a type whose values hold a handle (an opaque type, a function) is refused with the reason.

Both packages must have been generated from the same definition of the type, or one program would read the other’s values at the wrong layout. Every generated type carries its layout fingerprint (a digest of its constructors, their fields and every type they reach, with the Lean version), and a package using an extern type checks the providing package’s before anything runs: at compile time in Rust, when the package is loaded in Go (init), Python (import), Swift and C (the program’s first use), and TypeScript (module evaluation). A mismatch names the type and the package; regenerate both from the same Lean definition.

Environment variables

Entry points