# Set up lungo: instructions for coding agents

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:

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

```powershell
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:

```sh
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`:

| System | Install |
| --- | --- |
| macOS, Linux with Homebrew | `brew install machinefabric/tap/lungo` |
| Debian, Ubuntu (amd64, arm64) | apt, below |
| Fedora, RHEL (x86_64, aarch64) | dnf, below |
| Windows | PowerShell, below |
| any, with Rust 1.89+ | `cargo install lungo-cli` |

```sh
# 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
```

```sh
# 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
```

```powershell
# 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:

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

```toml
# 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+.

```sh
cargo add lungo
cargo add --build lungo-build
```

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

```rust
// 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

```toml
# 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.

| Language | Needs | Use |
| --- | --- | --- |
| Go | Go 1.22, cgo, a C compiler (MinGW-w64 GCC on Windows) | `go mod tidy`; import `<module>/<out>`. Functions return `(result, error)`; `Nat` is `*big.Int`. |
| Python | Python 3.9, CMake, a C compiler | `pip install ./<out>` into the venv; `from <name> import …`. Structures are frozen dataclasses; `Nat` is `int`. |
| Swift | Swift 5.9, macOS (targets macOS, iOS, iOS simulator) | `.package(path: "<out>")` in `Package.swift`; depend on the product `<out>/Package.swift` declares. |
| TypeScript | Node.js 20, or a browser | `"<name>": "file:./<out>"` in `package.json`, `npm install`; `import { load } from "<name>"`, `const lib = await load()`. `Nat` is `bigint`. Don't commit `<out>/program.wasm`; `lungo generate --link` makes it. |
| C | CMake 3.20, a C11 compiler | `add_subdirectory(<out>)`, `target_link_libraries(<target> PRIVATE <name>)`; header `<out>/include/<name>.h`. The first configure downloads lungo's runtime; offline, `lungo runtime fetch` and configure with `-D<NAME>_FETCH_LUNGO=OFF -DCMAKE_PREFIX_PATH=<runtime>` (`<NAME>` is `<name>` in upper case, `-` as `_`: `GEOMETRY_FETCH_LUNGO` for `geometry`). |

## 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):

```toml
# 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:

```lean
@[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:

```toml
# 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](https://machinefabric.com/lungo/docs/reference/errors.html).
- Missing dependency: `lake update` in `lean/`, or `lungo setup`.
- Otherwise: [diagnose build failures](https://machinefabric.com/lungo/docs/how-to/diagnose-build-failures.html);
  report to the user with the full output. Community: <https://discord.gg/D5w5ckFKrv>.

## Reference

- All docs, indexed: <https://machinefabric.com/lungo/llms.txt>
- [Configuration](https://machinefabric.com/lungo/docs/reference/configuration.html) ·
  [lungo command](https://machinefabric.com/lungo/docs/reference/lungo-cli.html) ·
  [generated packages](https://machinefabric.com/lungo/docs/reference/generated-packages.html) ·
  [platforms](https://machinefabric.com/lungo/docs/reference/platforms.html) ·
  [claims](https://machinefabric.com/lungo/docs/how-to/state-claims-about-exports.html)
- Tutorials: [Rust](https://machinefabric.com/lungo/docs/tutorials/first-crate.html) ·
  [Go](https://machinefabric.com/lungo/docs/tutorials/first-go-package.html) ·
  [Python](https://machinefabric.com/lungo/docs/tutorials/first-python-package.html) ·
  [Swift](https://machinefabric.com/lungo/docs/tutorials/first-swift-package.html) ·
  [TypeScript](https://machinefabric.com/lungo/docs/tutorials/first-typescript-package.html) ·
  [C](https://machinefabric.com/lungo/docs/tutorials/first-c-library.html)