lungo prende il programma di Lean nel punto in cui il compilatore di Lean ha finito di lavorarci. Questa pagina spiega qual è quel punto per Lean 4.34.1 e che cosa consegue da questa scelta.
Che cosa consegna Lean
Il compilatore di Lean abbassa le definizioni attraverso diverse fasi. La sua ultima fase per la
generazione del codice, l’LCNF impuro, viene abbassata ancora una volta in Lean.IR, la
rappresentazione che stampa il backend C di Lean. A quel punto Lean ha dedotto quali parametri
sono presi in prestito, quali valori sono inscatolati e quali no, ha inserito le operazioni sul
conteggio dei riferimenti e ha trasformato le occasioni di aggiornamento sul posto in controlli
espliciti.
Lean 4.34.1 conserva solo quest’ultima forma. La compilazione posticipata dell’LCNF è disattivata
per impostazione predefinita, quindi nei file compilati non sopravvive alcun LCNF; Lean.IR sì,
nei file .ir per i file che usano il sistema dei moduli e nei file .olean per gli altri. Il
worker legge quindi Lean.IR per ogni modulo nella chiusura degli import del programma,
compresi Init e Std, e lo codifica come Bridge IR.
La Bridge IR rappresenta Lean.IR istruzione per istruzione:
- istruzioni:
let,join,set,set_tag,uset,sset,inc,dec,del - terminatori:
case,ret,jmp,unreachable - espressioni:
ctor,reset,reuse,proj,uproj,sproj,fap,pap,ap,box,unbox, letterali,is_shared
L’unico cambiamento strutturale è che il codice lineare viene appiattito in blocchi, così il
lato Rust ricorre solo sulle annidature reali (punti di join e alternative dei case).
Conseguenze
Niente viene tradotto due volte. Le decisioni su prestito, inscatolamento e conteggio dei riferimenti sono di Lean, e il codice Rust le esegue come farebbe il backend C di Lean. Il Rust generato ha lo stesso comportamento in memoria del Lean nativo, compresi gli aggiornamenti distruttivi degli array non condivisi.
Una parte della Bridge IR non viene mai prodotta. Lean 4.34.1 espande ogni coppia
reset/reuse in is_shared, set, set_tag e del prima che l’IR sia definitiva, quindi
reset e reuse non arrivano mai a lungo da questa toolchain. Restano nella Bridge IR perché
fanno parte dell’IR di Lean e un’altra release potrebbe emetterle; il backend le implementa. I
test di lungo verificano sia che ogni istruzione emessa da questa toolchain venga esercitata,
sia che l’insieme di quelle che non emette mai sia esattamente questo.
I programmi sono chiusi rispetto alle loro dipendenze. Poiché il codice compilato di Init e
Std è a sua volta Lean.IR, la libreria standard segue lo stesso percorso del progetto: non
esiste un’implementazione Rust separata di List.map o di String.splitOn, solo delle
primitive del runtime sottostanti.
Il confine è versionato. La lettura di Lean.IR da parte del worker è un adattatore per una
release di Lean, con un proprio numero di versione, indipendente dalla versione della Bridge IR
e dal protocollo tra worker e build. Un cambiamento nell’IR di Lean cambia l’adattatore, non il
backend Rust, a meno che l’IR acquisisca nuove istruzioni.
Che cosa appartiene al programma
Il backend C di Lean inizializza un modulo inizializzando i suoi import ed eseguendo le sue
dichiarazioni [init], per fasi: un modulo che usa il sistema dei moduli esegue una fase di
esecuzione che esclude i suoi import meta e le dichiarazioni meta, che esistono solo in
fase di compilazione. Il worker segue la stessa regola per decidere quali moduli fanno parte del
programma. Un progetto può quindi usare l’intero elaboratore di Lean in un metaprogramma
importato con meta import senza che quel codice arrivi nel binario Rust.