Let your agent set up lungo

lungo compiles a Lean (Lake) project into a library for Rust, Go, Python, Swift, TypeScript (WebAssembly) or C. Theorems marked @[lungo_claim] ship with the package as proved claims.

Ask the user before sudo or editing files they did not ask about. If a step fails, stop and report the command and its output.

1. Detect

• Platform: uname -sm, or $env:PROCESSOR_ARCHITECTURE on Windows. Supported: macOS arm64 and x86_64, Linux x86_64 and arm64, Windows x86_64.
• Language, from the project root: Cargo.toml Rust; go.mod Go; pyproject.toml, setup.py or requirements.txt Python; Package.swift or an Xcode project Swift; package.json TypeScript; CMakeLists.txt or C sources C; only a lakefile, Lean alone. None, or several: ask which language will call the Lean code.

2. Lean

If elan --version fails, install elan:

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

curl -O --location https://elan.lean-lang.org/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1

Then, in a new shell:

elan toolchain install leanprover/lean4:v4.34.1

This is the only supported toolchain; the project’s lean-toolchain must name it exactly, or lungo fails with LNG0102.

3. The lungo command

Skip for Rust. Otherwise install it one of these ways, then check lungo --version:

# apt
curl -fsSL https://release.machinefabric.com/packages/keys/repo-signing-prod.asc \
  | sudo gpg --dearmor -o /usr/share/keyrings/machinefabric.gpg
echo "deb [signed-by=/usr/share/keyrings/machinefabric.gpg] https://release.machinefabric.com/packages/apt stable main" \
  | sudo tee /etc/apt/sources.list.d/machinefabric.list
sudo apt update && sudo apt install lungo

# dnf
sudo tee /etc/yum.repos.d/machinefabric.repo >/dev/null <<'EOF'
[machinefabric]
name=MachineFabric
baseurl=https://release.machinefabric.com/packages/rpm/$basearch
enabled=1
gpgcheck=1
repo_gpgcheck=1
gpgkey=https://release.machinefabric.com/packages/keys/repo-signing-prod.asc
EOF
sudo dnf install lungo

# Windows: latest release from the manifest, digest checked, added to the user's PATH
$manifest = Invoke-RestMethod https://release.machinefabric.com/lungo-cli/manifest
$version = $manifest.channels.release.latestVersion
$archive = $manifest.channels.release.versions.$version.platforms.'windows-x86_64'.installers[0]
Invoke-WebRequest $archive.path -OutFile $archive.name
if ((Get-FileHash $archive.name -Algorithm SHA256).Hash -ne $archive.sha256) { throw "the archive does not match the manifest's digest" }
$dir = "$env:LOCALAPPDATA\Programs\lungo-$version"
Expand-Archive $archive.name -DestinationPath $dir
[Environment]::SetEnvironmentVariable('Path', [Environment]::GetEnvironmentVariable('Path', 'User') + ";$dir\lungo", 'User')
$env:Path += ";$dir\lungo"

The same manifest (https://release.machinefabric.com/lungo-cli/manifest) lists a .tar.gz with its sha256 for darwin-arm64, darwin-x86_64, linux-x86_64 and linux-arm64; it holds lungo/lungo.

4. The Lake project

Put it in lean/. If one exists, check that lean-toolchain names the toolchain above and that lake-manifest.json exists; lungo setup installs the toolchain, fetches locked dependencies and prepares lungo’s worker. Otherwise create one:

mkdir lean
echo 'leanprover/lean4:v4.34.1' > lean/lean-toolchain

# lean/lakefile.toml
name = "geometry"
version = "0.1.0"
defaultTargets = ["Geometry"]

[[lean_lib]]
name = "Geometry"

Write the definitions in lean/Geometry.lean, inside namespace Geometry (ask the user what they should be). Then (cd lean && lake update) and commit lake-manifest.json. lungo never fetches dependencies: run lake update after adding one.

5. Rust

Needs Rust 1.89+.

cargo add lungo
cargo add --build lungo-build

// build.rs
fn main() -> lungo_build::Result<()> {
    lungo_build::compile_lean("lean")
}

// src/lib.rs: the module is named after the Lake package
pub mod geometry {
    lungo::include_lean!("geometry");
}

cargo build (the first takes minutes: lungo builds its Lean worker once). Lean structures become structs, functions plain functions, Nat is lungo::Nat.

6. Go, Python, Swift, TypeScript, C

# lungo.toml, at the project root; one table per language
project = "lean"

[go]          # or [python], [swift], [ts], [c]
out = "geometry"

Run lungo generate (prints generated go into geometry) and add .lungo/ to .gitignore. Without a lungo.toml: lungo generate --go_out=DIR (--python_out, --swift_out, --ts_out, --c_out).

<out> is the output directory. <name> is the Lake package’s name: lowercased in Go, Python and TypeScript, - as _ in C, UpperCamelCase as Swift’s module.

7. Verify

• Rust: cargo build && cargo test.
• Others: lungo check (builds; reports exports and proved claims), then the project’s tests.
• Committed generated code: lungo generate --verify in CI; it fails with LNG0110 listing every changed file.

8. Claims (optional)

Add lungo’s Lean library at the tag of the lungo in use (lungo --version, or the lungo crate’s version):

# lean/lakefile.toml
[[require]]
name = "lungo"
git = "https://github.com/machinefabric/lungo-rs"
rev = "v<version>"
subDir = "lean"

(cd lean && lake update), then import Lungo and mark the theorem:

@[lungo_claim "lungo.law" subject area scale]
theorem area_scale (k : Nat) (r : Rect) : area (scale k r) = k * k * area r := by
  simp only [area, scale]
  rw [Nat.mul_mul_mul_comm]

lungo assurance reports each export’s claims, trust and assumptions. To fail the build when a claim is missing or unproved:

# lungo.toml
[assurance]
require-claims = ["Geometry.area", "Geometry.scale"]

In Rust: lungo_build::configure().require_claims("Geometry.area").compile_lean("lean").

Errors

• error[LNGxxxx]: look the code up in errors.
• Missing dependency: lake update in lean/, or lungo setup.
• Otherwise: diagnose build failures; report to the user with the full output. Community: https://discord.gg/D5w5ckFKrv.

Reference

• All docs, indexed: https://machinefabric.com/lungo/llms.txt
• Configuration · lungo command · generated packages · platforms · claims
• Tutorials: Rust · Go · Python · Swift · TypeScript · C