The lungo command

lungo generates code from a Lean program the way protoc does from .proto files: one command, one output directory per language, and plugins for further languages.

lungo [OPTIONS] <COMMAND>
lungo generate --c_out=gen/c --go_out=gen/go --python_out=gen/py --rust_out=gen/rust

Install

With Homebrew, apt, dnf, Cargo, or a direct download for macOS, Linux and Windows: see installing lungo. Built from lungo-rs, lungo is a development build (see the runtime).

Configuration

The configuration is lungo.toml in the current directory, another file given with --config, or the Lake project given with --project and the default settings (see configuration). Giving both a file and --project is an error.

These options are global: they may precede or follow the command.

generate

lungo generate [--<language>_out=DIR]... [--<language>_opt=KEY=VALUE[,KEY=VALUE]...]... [--runtime-dir DIR] [--wasi-sdk DIR] [--verify | --link]

Generated packages describes each language’s package. DIRs on the command line are relative to the current directory; the configuration’s out directories to the configuration file. Without any --<language>_out, generate writes the outputs the configuration names (every language table with out, and [rust] with out-dir); with none, it fails (LNG0107). --<language>_opt adds options to the language’s options and overrides them; rust has no options on the command line (its settings are typed: see configuration).

Each output directory belongs to lungo: it is replaced as a whole, and a directory lungo did not create (one without its build-info.json) is never replaced (LNG0107). An output whose inputs (the Lean project, the toolchain, lungo, the generator and its options, the trust and assurance policies) are unchanged, and which still holds exactly the files it generated (none edited, removed or added since), is reused: generate prints up to date: <language> <DIR> instead of generated <language> into <DIR>. The project is analyzed once for every output (once more for ts, whose target is 32-bit WebAssembly).

Generated code is often committed, so that a package’s users need neither Lean nor lungo. --verify checks that it is current: it generates every output without writing, compares each directory’s generated sources with it, prints verified: <language> <DIR> for each that matches, and fails with LNG0110 naming every file that changed, is missing or is extra. Neither build-info.json nor a platform product is compared.

A platform product is a file an output links for the machine that writes it: the TypeScript binding’s program.wasm, the program linked with the WebAssembly runtime. It runs on every platform, but its bytes depend on the machine that built the runtime it links, so two machines link different modules from the same sources. It is a build product: generated with the sources, never committed (ignore it in version control; npm packs it from the package’s files). --link writes only the platform products, for this machine, into outputs whose sources are current — linked: <language> <DIR> for this machine — leaving the sources as they are; where they are not current it links nothing and fails with LNG0110. A checkout runs --link before it tests the TypeScript binding.

assurance

lungo assurance [DECLARATION] [--format human|json] [--claim-kind RELATION]... [--facility NAME]...
                [--assumption NAME]... [--trust-issue ISSUE]... [--policy] [--compose FILE]...

Reports, export by export, what the program’s Lean code claims and proves of it, what its proofs do not cover (its trust) and what its claims assume of the host, keeping the three apart. It builds and analyzes the project as check does, and refuses a program whose assurance records are invalid (LNG0701–LNG0710): a report of them would mislead.

The human report starts with the program and its provenance (Lean version and commit, lungo version, assurance schema), then one block per export, with the sections == Claims ==, == Trust ==, == Assumptions == and == Facilities ==; an empty section reads (none). A claim’s status is written in brackets, [proved] or [incomplete] (resting on sorry), with its relation, the specifications it is about and the assumptions it rests on. An assumption is written [assumed] with what it says — its definition when it is one, otherwise its type — and its facility:

    [assumed] Polyglot.ScalesMonotonically : ∀ (a b : Nat), a ≤ b → Polyglot.hostScale a ≤ Polyglot.hostScale b (of Polyglot.Scaler)

An async export is marked (async). --format json prints the same as a JSON object: schema_version, program, provenance, exports (as in assurance.json), the claims about them, policy (the violations, with --policy) and composition (the mismatches).

Filters of different kinds must all match; values of one kind match if any does.

--compose checks that separately generated packages describe every record they share (a specification, claim, facility or assumption, by Lean name) the same way: from the same package, with the same fingerprint. A record described differently — a specification, or a definition of the workspace it uses, changed in one package and not regenerated in the other — is reported as LNG0708 with each document’s package and fingerprint. With a configuration (a lungo.toml, --config or --project), the project’s own document is one of those compared; without one, the files given are compared with each other, and at least two are needed. A file that is not an assurance document lungo reads is LNG0711.

The runtime

Every language runs the program on the same runtime, prebuilt for every platform and published with each lungo release: generated packages refer to the release’s runtime archives by URL and SHA-256 digest (the C package’s CMake downloads and checks it; the Go, Python, Swift and TypeScript support libraries carry it). A release of lungo knows its runtime release from the manifest built into it.

A development build of lungo (built from source) knows no release. Generating a package other than Rust then needs a local distribution: a directory laid out as a release (runtime/, wasm/, go/, python/, lungo-swift/, ts/), built from lungo-rs with cargo run -p lungo-dist -- local --out DIR, and given with --runtime-dir DIR. With --python PATH it also holds lungo-py’s wheel for this machine in wheels/, for pip to find (--find-links DIR/wheels) when it builds a generated Python package. Without one the command fails with LNG0108. The generated packages then refer to that directory, so they build only on that machine.

lungo runtime fetch [--target TRIPLE]
lungo runtime path [--target TRIPLE]
lungo runtime verify [--target TRIPLE]

A download whose digest differs from the release’s is discarded and reported as LNG0109. The runtime package holds include/lungo.h, the static and shared libraries in lib/, lib/cmake/lungo/lungoConfig.cmake and lib/pkgconfig/lungo.pc.

Updating

lungo self update

Replaces this lungo with the latest release of the channel it was published on, and prints lungo <old> -> <new>, or lungo <version> is the latest release when there is nothing newer. It reads the release manifest of the registry this lungo was published in (the one installing lungo names), and installs a release only when all of this holds:

• the manifest’s signature chains to the keys built into this lungo: a certificate for the release key, signed by two of those keys, valid now, and the manifest signed by that release key;
• the archive has the size and the SHA-256 digest the manifest lists;
• the command in the archive runs and reports the version it was published as.

Anything else is LNG0112, and the installed command is left as it is. The new command takes the place of the old one in one step, where the old one is, so lungo on your PATH is the new release from then on. On Windows the running command cannot be removed: it is left beside the new one as lungo.exe.old, and the next update removes it.

Two kinds of lungo are not updated this way, and say what updates them (LNG0111):

A package manager’s lungo is recognized by the file installed-by its package puts beside the command. A lungo installed where you cannot write — /usr/local/bin, with sudo install — is updated with the same rights: sudo lungo self update.

Other commands

Errors are printed as error[LNGxxxx]: … (see errors) and the command exits with status 1 (assurance has two more statuses: see above).

Example

$ lungo generate --go_out=gen/formal --python_out=gen/py
generated go into gen/formal
generated python into gen/py
$ lungo inspect Formal.step
Formal.step : Formal.Sess → Formal.Op → Bool × Formal.Sess
module: Formal.Session
source: lean/Formal/Session.lean
exported: yes
  == Claims ==
    [proved] lungo.preserves Formal.step_implements (of Formal.Spec)
  == Trust ==
    (none)
  == Assumptions ==
    (none)
  == Facilities ==
    (none)
  == Trust, in full ==
    axioms: (none)
    depends on sorry: false
    unsafe dependencies: (none)
    partial dependencies: (none)
    extern dependencies: lean_nat_add
compiled: (obj, u8) -> obj in module Formal.Session
compiler auxiliaries: Formal.step._boxed