lungo generates code from Lean projects: a Rust module at Cargo build time, and with the
lungo command packages for C, Go, Python, Swift (and Objective-C) and TypeScript. Lean’s
own frontend checks and compiles the project; lungo turns the compiled program into each
language with an idiomatic API, running on one runtime. Every package carries what the
project proves of its exports, the host facilities they need, and what those proofs assume.
Tutorials
Start here if you are new to lungo.
- Your first Rust crate built from Lean
- Your first Go package built from Lean
- Your first Python package built from Lean
- Your first Swift package built from Lean
- Your first TypeScript package built from Lean
- Your first C library built from Lean
How-to guides
- How to call Rust functions from Lean
- How to call host code from Lean (Go, Python, Swift, TypeScript, C)
- How to call async host operations
- How to state claims about exports
- How to declare facilities and assumptions
- How to write runtime monitors and test oracles
- How to compose assurance across packages
- How to define a semantic model
- How to distribute generated packages
- How to write a generator plugin
- How to run a Lean program’s
mainfrom Rust - How to derive
serdeand other traits for generated types - How to share types between Lean projects
- How to see what lungo generated for a declaration
- How to enforce trust and assurance policies
- How to compare generated Rust with Lean’s native backend
- How to bound the resources a build may use
- How to diagnose a failing lungo build
Reference
- Configuration
- The
lungocommand - Generated packages (C, Go, Python, Swift, TypeScript)
- The C API (
lungo.h) - Wire format
- Generator plugins
- Generated code
- The assurance document (
assurance.json) - The Lean library
- Lean types in Rust
- Errors
- Supported platforms
The Rust API of the lungo and lungo-build crates is documented by rustdoc:
cargo doc -p lungo -p lungo-build --open.