lungo genera codice da progetti Lean: un modulo Rust durante la build di Cargo e, con il
comando lungo, pacchetti per C, Go, Python, Swift (e Objective-C) e TypeScript. Il frontend
di Lean controlla e compila il progetto; lungo trasforma il programma compilato in ciascun
linguaggio con un’API idiomatica, eseguita su un unico runtime. Ogni pacchetto porta ciò che il
progetto dimostra dei suoi export, le facility dell’host di cui hanno bisogno e ciò che quelle
dimostrazioni assumono.
Tutorial
Inizia da qui se lungo è nuovo per te.
- Il tuo primo crate Rust costruito da Lean
- Il tuo primo pacchetto Go costruito da Lean
- Il tuo primo pacchetto Python costruito da Lean
- Il tuo primo pacchetto Swift costruito da Lean
- Il tuo primo pacchetto TypeScript costruito da Lean
- La tua prima libreria C costruita da Lean
Guide pratiche
- Come chiamare funzioni Rust da Lean
- Come chiamare codice dell’host da Lean (Go, Python, Swift, TypeScript, C)
- Come chiamare operazioni asincrone dell’host
- Come dichiarare claim sugli export
- Come dichiarare facility e assunzioni
- Come scrivere monitor a runtime e oracoli di test
- Come comporre le garanzie tra pacchetti
- Come definire un modello semantico
- Come distribuire i pacchetti generati
- Come scrivere un plugin generatore
- Come eseguire il
maindi un programma Lean da Rust - Come derivare
serdee altri trait per i tipi generati - Come condividere tipi tra progetti Lean
- Come vedere che cosa lungo ha generato per una dichiarazione
- Come imporre politiche di fiducia e di garanzia
- Come confrontare il Rust generato con il backend nativo di Lean
- Come limitare le risorse che una build può usare
- Come diagnosticare una build di lungo che fallisce
Riferimento
- Configurazione
- Il comando
lungo - Pacchetti generati (C, Go, Python, Swift, TypeScript)
- L’API C (
lungo.h) - Formato di trasmissione
- Plugin generatori
- Codice generato
- Il documento di garanzia (
assurance.json) - La libreria Lean
- I tipi Lean in Rust
- Errori
- Piattaforme supportate
L’API Rust dei crate lungo e lungo-build è documentata da rustdoc:
cargo doc -p lungo -p lungo-build --open.