Documentazione di lungo

Piattaforme supportate

Le toolchain Lean supportate, le piattaforme host e target, le piattaforme del runtime e ciò di cui ha bisogno ciascun binding di linguaggio.

In questa sezione

Toolchain Lean

Toolchain Commit Stato
leanprover/lean4:v4.34.1 5045d0056413266e57c625dcd7c365b10e377c52 supportata

Il lean-toolchain di un progetto deve indicare esattamente una toolchain supportata; qualsiasi altro valore, compresi i nomi mobili (stable, nightly), fallisce con LNG0102 prima che venga compilato qualcosa. Il lean --version della toolchain installata deve corrispondere a quella fissata.

Rust

Rust 1.89 o successivo, edizione 2024.

Host e modalità

Host PureRust LeanOracle Limite di memoria del worker
Linux sì sì sì
macOS sì sì no (LNG0104)
Windows, target *-windows-msvc sì no (LNG0104) sì
Windows, target *-windows-gnu sì sì sì
  • PureRust genera codice per qualsiasi target Rust, compresi i target di cross-compilazione; il codice generato non collega alcun runtime di Lean né codice C.
  • LeanOracle collega il runtime nativo di Lean dalla toolchain dell’host e non può fare cross-compilazione. Su Windows richiede l’ABI GNU, per cui è compilato il runtime di Lean.

Il runtime precompilato

Ogni release pubblica il runtime (lungo runtime fetch --target <triple>) per:

Target Statica Condivisa Usato da
x86_64-unknown-linux-gnu, aarch64-unknown-linux-gnu (glibc 2.28 o successiva) sì sì C, Go, Python
x86_64-unknown-linux-musl, aarch64-unknown-linux-musl sì   C
x86_64-apple-darwin, aarch64-apple-darwin (macOS 12 o successivo) sì sì C, Go, Python, Swift
aarch64-apple-ios, aarch64-apple-ios-sim, x86_64-apple-ios (iOS 15 o successivo) sì   C, Swift
x86_64-pc-windows-msvc sì sì C, Python
x86_64-pc-windows-gnu sì sì C, Go (cgo compila con MinGW-w64)
wasm32-wasip1 sì   TypeScript

I runtime musl sono solo librerie statiche: le build musl sono crt-static, con cui Rust non produce alcuna libreria condivisa.

I target Apple sono anche combinati in un unico XCFramework (macOS universale, iOS, simulatore iOS universale), usato dal pacchetto Swift.

Binding dei linguaggi

Linguaggio Richiede Piattaforme
C CMake 3.20, un compilatore C11 ogni target qui sopra
Go Go 1.22, cgo con un compilatore C (GCC di MinGW-w64 su Windows) Linux (amd64, arm64), macOS (amd64, arm64), Windows (amd64)
Python Python 3.9, CMake, un compilatore C per installare dai sorgenti Linux (x86_64, aarch64, glibc), macOS (x86_64, arm64), Windows (x86_64)
Swift, Objective-C Swift 5.9 macOS, iOS, simulatore iOS
TypeScript Node.js 20, oppure un browser ovunque giri WebAssembly; niente thread, processi figli, socket, segnali o timer (LNG0408)

lungo stesso gira su Linux (x86_64, aarch64), macOS (x86_64, arm64) e Windows (x86_64). Il comando rilasciato è collegato staticamente su Linux (musl) e compilato per l’ABI GNU su Windows, che è anche il target predefinito dei suoi comandi runtime.

Requisiti del progetto Lake

  • lean-toolchain, lakefile.toml o lakefile.lean, e lake-manifest.json.
  • Le dipendenze bloccate nel manifest devono essere materializzate (lake update, oppure lungo setup). Le build non risolvono, scaricano né aggiornano mai le dipendenze.
  • I moduli radice appartengono al pacchetto radice del progetto.