# lungo

> Generate Rust, C, Go, Python, Swift and TypeScript from ordinary Lake projects.

## For agents

- [Set up lungo: instructions for coding agents](https://machinefabric.com/lungo/agents.md): How an AI coding agent installs lungo on macOS, Linux or Windows and starts using it in a Rust, Go, Python, Swift, TypeScript, C or Lean project.

## Start

- [Overview](https://machinefabric.com/lungo/docs/index.html): Tutorials, how-to guides, reference and explanation for generating Rust, C, Go, Python, Swift and TypeScript from Lean projects.
- [Installing lungo](https://machinefabric.com/lungo/docs/install.html): Every way to install the lungo command: Homebrew, apt, dnf, Cargo, and a direct download for macOS, Linux and Windows.

## Tutorials

- [Your first Rust crate built from Lean](https://machinefabric.com/lungo/docs/tutorials/first-crate.html): Write Lean definitions and a proof, build them into a Rust crate, call them from Rust, and make the proof part of what the crate says about itself.
- [Your first Go package built from Lean](https://machinefabric.com/lungo/docs/tutorials/first-go-package.html): Write Lean definitions and a proof, generate a Go package from them with lungo, and call it from a Go program.
- [Your first Python package built from Lean](https://machinefabric.com/lungo/docs/tutorials/first-python-package.html): Write Lean definitions and a proof, generate a Python package from them with lungo, and call it from Python.
- [Your first Swift package built from Lean](https://machinefabric.com/lungo/docs/tutorials/first-swift-package.html): Write Lean definitions and a proof, generate a Swift package from them with lungo, and call it from Swift.
- [Your first TypeScript package built from Lean](https://machinefabric.com/lungo/docs/tutorials/first-typescript-package.html): Write Lean definitions and a proof, generate an npm package running on WebAssembly with lungo, and call it from JavaScript.
- [Your first C library built from Lean](https://machinefabric.com/lungo/docs/tutorials/first-c-library.html): Write Lean definitions and a proof, generate a C library from them with lungo, and call it from a C program built with CMake.

## How-to guides

- [How to call Rust functions from Lean](https://machinefabric.com/lungo/docs/how-to/call-rust-from-lean.html): Declare a facility's operations in Lean, implement them in Rust, and map each symbol to its Rust function.
- [How to call host code from Lean](https://machinefabric.com/lungo/docs/how-to/call-host-code-from-lean.html): Declare a facility of operations in Lean and implement it in Go, Python, Swift, TypeScript or C.
- [How to declare facilities and assumptions](https://machinefabric.com/lungo/docs/how-to/declare-facilities-and-assumptions.html): Declare what the host provides as a facility of operations, state what claims assume of it, and implement it in each language.
- [How to call async host operations](https://machinefabric.com/lungo/docs/how-to/call-async-host-operations.html): Write Lean programs that ask the host to perform operations asynchronously, call them as native async functions in each language, and prove what they do against a model.
- [How to distribute generated packages](https://machinefabric.com/lungo/docs/how-to/distribute-generated-packages.html): Publish a package lungo generated as a Go module, a Python wheel, a Swift package, an npm package or a CMake library.
- [How to write a generator plugin](https://machinefabric.com/lungo/docs/how-to/write-a-generator-plugin.html): Generate a package in a language lungo does not build in, with a lungo-gen-<language> program.
- [How to run a Lean program's main from Rust](https://machinefabric.com/lungo/docs/how-to/run-a-lean-program.html): Build a Lean executable as a Rust binary, and run several Lean programs from one binary.
- [How to derive serde and other traits for generated types](https://machinefabric.com/lungo/docs/how-to/shape-generated-types.html): Add serde derives and other attributes to generated types and fields, implement Debug yourself, and omit documentation comments.
- [How to share types between Lean projects](https://machinefabric.com/lungo/docs/how-to/share-types-between-projects.html): Use the types generated for one Lake package in the package generated for a Lake package that requires it, in Rust and in every other language.
- [How to see what lungo generated for a declaration](https://machinefabric.com/lungo/docs/how-to/inspect-generated-code.html): Find a Lean declaration's Rust name and signature, its compiler output, its dependencies and what is proved of it with the lungo command.
- [How to enforce trust and assurance policies](https://machinefabric.com/lungo/docs/how-to/enforce-trust-policies.html): Fail the build when an export or the proof of a claim depends on sorry, non-standard axioms or unsafe code, require proved claims and forbid assumptions, and audit what exports depend on.
- [How to state claims about exports](https://machinefabric.com/lungo/docs/how-to/state-claims-about-exports.html): Prove what exported Lean definitions do, register the theorems as claims, require them in the build, and read them back in every language.
- [How to write runtime monitors and test oracles](https://machinefabric.com/lungo/docs/how-to/write-runtime-monitors.html): Check a running system against a Lean protocol with a proved monitor, and test hand-written code against a proved oracle.
- [How to compose assurance across packages](https://machinefabric.com/lungo/docs/how-to/compose-assurance-across-packages.html): Check that separately generated packages describe the specifications, claims, facilities and assumptions they share the same way, with lungo assurance --compose.
- [How to define a semantic model](https://machinefabric.com/lungo/docs/how-to/define-a-semantic-model.html): Give a Lake package its own specification kinds and claim relations, which lungo carries into every package without any change to lungo.
- [How to compare generated Rust with Lean's native backend](https://machinefabric.com/lungo/docs/how-to/compare-with-native-lean.html): Build one Lean project in PureRust and LeanOracle modes in one crate, and check that both give the same results.
- [How to bound the resources a build may use](https://machinefabric.com/lungo/docs/how-to/bound-the-worker.html): Limit the time, processor time and memory of the lungo worker, and isolate it from your environment.
- [How to diagnose a failing lungo build](https://machinefabric.com/lungo/docs/how-to/diagnose-build-failures.html): Get from a failing cargo build to its cause, by error code.

## Reference

- [Configuration](https://machinefabric.com/lungo/docs/reference/configuration.html): Every lungo.toml key and lungo_build::Builder setting, with its default.
- [The lungo command](https://machinefabric.com/lungo/docs/reference/lungo-cli.html): lungo generate and the other commands: generating packages in every language, inspecting the program, and the runtime.
- [Generated packages](https://machinefabric.com/lungo/docs/reference/generated-packages.html): What lungo generate writes for C, Go, Python, Swift and TypeScript: package layouts, how Lean types map to each language, names, errors and threads.
- [The C API (lungo.h)](https://machinefabric.com/lungo/docs/reference/c-api.html): The lungo runtime's C interface: the value API C and Objective-C programs use, and the program API generated code uses.
- [Wire format](https://machinefabric.com/lungo/docs/reference/wire-format.html): The binary encoding of Lean values between a program and the language bindings: type expressions, values, type tables, signatures, handles, host functions and async programs.
- [Generator plugins](https://machinefabric.com/lungo/docs/reference/plugins.html): The protocol between the lungo command and generator plugins: the GenerateRequest and GenerateResponse JSON documents.
- [Generated code](https://machinefabric.com/lungo/docs/reference/generated-code.html): The files a build publishes, the generated module, its metadata, and the JSON reports.
- [assurance.json](https://machinefabric.com/lungo/docs/reference/assurance-json.html): The assurance document every generated output carries: its schema, field by field, its ordering, fingerprints, and how each language reads it.
- [The Lean library](https://machinefabric.com/lungo/docs/reference/lean-library.html): lungo's Lean library: the attributes that register specifications, claims, facilities, assumptions and roles, lungo's relations and kinds, and the definitions claims are stated with.
- [Lean types in Rust](https://machinefabric.com/lungo/docs/reference/type-mapping.html): How each Lean type appears in the generated Rust API, and the serde feature.
- [Errors](https://machinefabric.com/lungo/docs/reference/errors.html): Every lungo error code, what causes it, and what to do about it.
- [Supported platforms](https://machinefabric.com/lungo/docs/reference/platforms.html): The supported Lean toolchains, host and target platforms, the runtime's platforms, and what each language binding needs.

## Explanation

- [Architecture](https://machinefabric.com/lungo/docs/explanation/architecture.html): How lungo's pieces fit together: why Lean compiles the program before lungo translates it, and how one program reaches every language on one runtime.
- [The runtime distribution](https://machinefabric.com/lungo/docs/explanation/distribution.html): Why every language runs on one prebuilt runtime, how it is distributed, and what a user of a generated package has to trust.
- [The compiler boundary](https://machinefabric.com/lungo/docs/explanation/compiler-boundary.html): Where lungo takes the program from Lean's compiler for Lean 4.34.1, and what follows from that choice.
- [The runtime](https://machinefabric.com/lungo/docs/explanation/runtime.html): How lungo's Rust runtime relates to Lean's: its object model, reference counting, and IO.
- [Trust and verification](https://machinefabric.com/lungo/docs/explanation/trust-and-verification.html): What a Lean proof covers when the definition runs as Rust or another language, how each link is checked, what a claim rests on, and what the build isolates.
- [Formal assurance](https://machinefabric.com/lungo/docs/explanation/formal-assurance.html): What a generated package can say about its exports: claims proved in Lean, the assumptions they rest on, and how to read them.