Il codice Lean compilato presuppone un runtime: un modello a oggetti, il conteggio dei riferimenti, numeri grandi, stringhe, array, chiusure, task e IO. lungo porta il proprio, scritto in Rust. Questa pagina spiega come si rapporta a quello di Lean.
Un port, non una reinterpretazione
lungo-runtime è un port di lean.h di Lean e del suo runtime C++. Gli oggetti hanno
esattamente il layout di Lean (un’intestazione con conteggio dei riferimenti, dimensione ed
etichetta, seguita dai campi), e i valori piccoli sono scalari etichettati come in Lean. Il
conteggio dei riferimenti ha la semantica di Lean, compresi gli oggetti condivisi tra thread e
gli oggetti persistenti che non vengono mai liberati. La liberazione di una struttura grande è
iterativa, come in Lean, così non può esaurire lo stack.
Mantenere identico il layout è ciò che fa funzionare il resto del progetto. Il codice compilato
può essere generato istruzione per istruzione, perché ogni istruzione significa la stessa cosa
che nel backend C di Lean. E le conversioni della facciata leggono gli oggetti allo stesso modo,
che provengano dal runtime Rust o dal runtime nativo di Lean in modalità LeanOracle, ed è ciò
che rende significativo un confronto chiamata per chiamata tra i due.
Un runtime per ogni linguaggio
Lo stesso runtime serve i programmi generati in C, per ogni linguaggio tranne Rust. Compilato
con la sua ABI C è liblungo, e lungo.h lo dichiara come lean.h dichiara il runtime di
Lean: il layout degli oggetti e i percorsi rapidi dell’inscatolamento e del conteggio dei
riferimenti sono funzioni inline dell’header, identiche alle definizioni Rust che
rispecchiano, e ogni primitiva è una funzione esportata con la firma registrata nel registro.
Il C generato compilato su di esso si comporta come il livello del compilatore Rust, cosa che i
programmi di conformità verificano.
Il runtime si compila anche per WebAssembly (wasm32-wasip1). Lì ha un solo thread: i task di
Lean vengono eseguiti quando vengono creati, come li esegue il runtime di Lean senza un gestore
dei task, e le primitive che richiedono thread del sistema operativo, processi figli, socket,
segnali o timer sono escluse, così un programma che le usa viene rifiutato quando viene
generato invece di fallire quando viene eseguito.
Le primitive sono dichiarate, non presunte
Il codice Lean raggiunge le funzionalità native tramite simboli @[extern]. Ogni primitiva
implementata dal runtime è dichiarata con la sua firma a livello C: la rappresentazione di
ciascun parametro e se è preso in prestito o posseduto. Quando un programma usa un simbolo
extern, la generazione del codice confronta la firma della primitiva con la dichiarazione di
Lean e riconcilia il prestito con operazioni esplicite sul conteggio dei riferimenti, così le
due cose non possono divergere in silenzio.
Un simbolo extern viene risolto, nell’ordine, in:
- una definizione Lean che esporta il simbolo con
@[export](Lean implementa alcuni dei propri extern in Lean, e questi vengono compilati come qualsiasi altro codice); - una primitiva del runtime;
- una funzione dell’applicazione mappata con
rust_extern.
Qualsiasi altra cosa è un errore di build. I test del runtime lo confrontano con inventari
generati dalla toolchain: ogni simbolo extern di Init e di Std è implementato, e nessuno è
oscurato.
Codice Lean dentro il runtime
Il runtime C di Lean stesso chiama alcune funzioni scritte in Lean: costruisce i valori
IO.Error con i costruttori di Lean, li rende con IO.Error.toString, avvolge i flussi
standard con IO.FS.Stream.ofHandle e stampa i panic con IO.eprintln. Il runtime Rust fa lo
stesso. Ogni programma include queste definizioni Lean compilate e le registra all’avvio. Il
layout di IO.Error vive quindi in un solo posto, il codice Lean compilato, come nel Lean
nativo.
Fedele anche nei dettagli
Corrispondere a Lean significa corrispondere al comportamento che gli utenti possono
osservare, non solo ai risultati. Gli handle IO fanno buffering come i FILE del C; la
formattazione dei float segue quella del C; un processo figlio che non riesce a eseguire il suo
programma riporta il fallimento dal figlio creato con fork ed esce come fa quello di Lean, il
che riproduce perfino il modo in cui exit del C svuota l’output che il genitore aveva nel
buffer. I test di conformità confrontano standard output, standard error e codici di uscita
byte per byte con gli eseguibili di Lean stesso.