lungo

lungo · per gli agenti di programmazione

Fai configurare lungo al tuo agente

Dai questa riga a Claude Code, Codex, Cursor o a qualsiasi agente di programmazione che lavora nel tuo progetto. Installa lungo per il tuo sistema, poi lo configura per il linguaggio del progetto.

Leggi https://machinefabric.com/lungo/agents.md e configura lungo in questo progetto.

lungo compila un progetto Lean (Lake) in una libreria per Rust, Go, Python, Swift, TypeScript (WebAssembly) o C. I teoremi marcati @[lungo_claim] accompagnano il pacchetto come claim dimostrati.

Chiedi all’utente prima di usare sudo o di modificare file di cui non ha parlato. Se un passaggio fallisce, fermati e riferisci il comando e il suo output.

1. Rileva

2. Lean

Se elan --version fallisce, installa 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

Poi, in una nuova shell:

elan toolchain install leanprover/lean4:v4.34.1

È l’unica toolchain supportata; il lean-toolchain del progetto deve nominarla esattamente, altrimenti lungo fallisce con LNG0102.

3. Il comando lungo

Non serve per Rust. Altrimenti installalo in uno di questi modi, poi controlla lungo --version:

Sistema Installazione
macOS, Linux con Homebrew brew install machinefabric/tap/lungo
Debian, Ubuntu (amd64, arm64) apt, qui sotto
Fedora, RHEL (x86_64, aarch64) dnf, qui sotto
Windows PowerShell, qui sotto
qualsiasi, con Rust 1.89+ cargo install lungo-cli 
# 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"

Lo stesso manifest (https://release.machinefabric.com/lungo-cli/manifest) elenca un .tar.gz con il suo sha256 per darwin-arm64, darwin-x86_64, linux-x86_64 e linux-arm64; contiene lungo/lungo.

4. Il progetto Lake

Mettilo in lean/. Se ne esiste già uno, controlla che lean-toolchain nomini la toolchain qui sopra e che lake-manifest.json esista; lungo setup installa la toolchain, scarica le dipendenze fissate e prepara il worker di lungo. Altrimenti creane uno:

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"

Scrivi le definizioni in lean/Geometry.lean, dentro namespace Geometry (chiedi all’utente quali debbano essere). Poi (cd lean && lake update) e fai il commit di lake-manifest.json. lungo non scarica mai dipendenze: esegui lake update dopo averne aggiunta una.

5. Rust

Serve 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 (la prima richiede qualche minuto: lungo compila una volta il suo worker Lean). Le strutture di Lean diventano struct, le funzioni semplici funzioni, Nat è 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"

Esegui lungo generate (stampa generated go into geometry) e aggiungi .lungo/ a .gitignore. Senza un lungo.toml: lungo generate --go_out=DIR (--python_out, --swift_out, --ts_out, --c_out).

<out> è la directory di destinazione. <name> è il name del pacchetto Lake: in minuscolo in Go, Python e TypeScript, con _ al posto di - in C, in UpperCamelCase come modulo Swift.

Linguaggio Serve Uso
Go Go 1.22, cgo, un compilatore C (MinGW-w64 GCC su Windows) go mod tidy; importa <module>/<out>. Le funzioni restituiscono (result, error); Nat è *big.Int.
Python Python 3.9, CMake, un compilatore C pip install ./<out> nel venv; from <name> import …. Le strutture sono dataclass immutabili; Nat è int.
Swift Swift 5.9, macOS (target macOS, iOS, simulatore iOS) .package(path: "<out>") in Package.swift; dipendi dal prodotto che dichiara <out>/Package.swift.
TypeScript Node.js 20, o un browser "<name>": "file:./<out>" in package.json, npm install; import { load } from "<name>", const lib = await load(). Nat è bigint. Non fare il commit di <out>/program.wasm; lo crea lungo generate --link.
C CMake 3.20, un compilatore C11 add_subdirectory(<out>), target_link_libraries(<target> PRIVATE <name>); header <out>/include/<name>.h. La prima configurazione scarica il runtime di lungo; offline, lungo runtime fetch e configura con -D<NAME>_FETCH_LUNGO=OFF -DCMAKE_PREFIX_PATH=<runtime> (<NAME> è <name> in maiuscolo, con _ al posto di -: GEOMETRY_FETCH_LUNGO per geometry).

7. Verifica

8. Claim (facoltativo)

Aggiungi la libreria Lean di lungo al tag del lungo in uso (lungo --version, o la versione del crate lungo):

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

(cd lean && lake update), poi import Lungo e marca il teorema:

@[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 riporta per ogni export i claim, la fiducia e le assunzioni. Per far fallire la build quando un claim manca o non è dimostrato:

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

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

Errori

Riferimenti