Un generatore per un linguaggio che lungo non integra è un plugin: un programma chiamato
lungo-gen-<language> nel PATH (lungo-gen-<language>.exe su Windows), eseguito da
lungo generate --<language>_out=DIR, come protoc esegue protoc-gen-<language>.
Il plugin legge una GenerateRequest come JSON dal suo standard input e scrive una
GenerateResponse come JSON sul suo standard output; il suo standard error viene mostrato se
fallisce. I generatori integrati ricevono esattamente la stessa richiesta. I tipi Rust di
entrambi i documenti sono lungo_build::codegen::plugin::{GenerateRequest, GenerateResponse}
(serde), che un plugin in Rust può usare direttamente. Vedi
come scrivere un plugin generatore.
GenerateRequest
| Campo | Significato |
|---|---|
protocol_version |
3. Un plugin rifiuta le versioni che non conosce. |
program |
name (il nome del programma), lean_version, lean_githash, bir_version, root_modules. |
boundary |
L’interfaccia del programma (sotto). |
program_files |
Il programma come C: percorsi (sotto program/) mappati sui contenuti, compreso lungo.h. Un pacchetto compila ogni file .c con program/ nel percorso degli include. |
runtime |
version (la release di lungo), abi_version (l’ABI C) e distribution: {"release": {"artifacts": {…}}} (gli archivi del runtime per target triple e xcframework, ciascuno {url, sha256}), oppure {"local": {"dir": …}} (una distribuzione locale: un percorso assoluto con separatori /, anche su Windows). |
options |
Le opzioni del generatore (--<language>_opt, options di [plugins.<language>]), stringhe per chiave. Un plugin rifiuta le chiavi che non conosce. |
assurance |
Il documento di garanzia del programma, come lo contiene assurance.json. lungo scrive assurance.json nell’output da sé; un plugin che espone il documento nel suo linguaggio (come fa ogni generatore integrato) ne incorpora esattamente il testo. |
extern_types |
I tipi del programma forniti da un altro pacchetto generato (extern-types di [plugins.<language>]): per nome Lean, {package, name} nei termini del linguaggio. Un plugin rifiuta quelli per cui il confine non ha un tipo, usa il tipo e il descrittore dell’altro pacchetto invece di generarne uno, e controlla l’impronta del layout dell’altro pacchetto prima che il programma venga eseguito. |
boundary
| Campo | Significato |
|---|---|
id |
L’identificatore C del programma. |
prefix |
Il prefisso dei simboli C del programma, <id>__. |
table |
La tabella dei tipi: types, ciascuno con name, params (un conteggio), repr, trivial ([constructor, field] oppure null), ctors (name, tag, size, usize, ssize, fields: name, kind, ty). |
types |
Per ogni tipo della tabella: lean_name, params (i nomi Lean dei suoi parametri), structure, opaque (i suoi valori sono handle: la voce della tabella non ha costruttori) e fingerprint (l’impronta del suo layout, SHA-256 in esadecimale minuscolo), che il pacchetto espone per i pacchetti che usano il tipo. |
functions |
Per ogni funzione esportata: lean_name, module, lean_type, symbol (il suo punto di ingresso C), type_params, params (name, ty), returns, source. Una funzione il cui returns è async restituisce il primo passo di un programma asincrono. |
facilities |
Per ogni facility che l’host implementa, per identificatore: id (come time.clock), lean_name, e operations, ciascuna con index (per set_host_extern), key, declaration, lean_type, params, returns. I parametri di tipo delle operazioni polimorfe sono valori opachi. |
async_facilities |
Per ogni facility asincrona a cui gli export chiedono operazioni: id, lean_name, op_type (l’indice del tipo di operazioni nella tabella), e operations, ciascuna con ctor (l’indice del costruttore), lean_name e answer (il tipo con cui riceve risposta). |
run_main |
Il simbolo di int32_t run_main(size_t argc, const char *const *argv), oppure null senza un main. |
set_host_extern |
void set_host_extern(size_t index, uint64_t callback): registra una funzione dell’host (vedi funzioni dell’host). |
types_symbol |
const lungo_types *types(void): la tabella dei tipi caricata. |
initialize |
void initialize(void): ogni punto di ingresso inizializza il programma al primo uso; richiede che ogni operazione di ogni facility sia registrata, e altrimenti termina il processo indicando la facility e l’operazione mancanti. I generatori integrati per i linguaggi con errori controllano che ogni facility sia installata prima di chiamare il programma, così che i loro utenti ricevano invece l’errore del linguaggio. |
I tipi (ty, returns) sono espressioni di tipo in JSON: "nat", "int", "bool",
"uint8", "uint16", "uint32", "uint64", "usize", "int8", "int16", "int32",
"int64", "isize", "float", "float32", "char", "string", "unit", "byte_array",
"float_array" per i tipi senza parti, {"option": t}, {"list": t}, {"array": t},
{"prod": [a, b]}, {"except": {"error": e, "value": v}},
{"function": {"params": […], "result": r}}, {"param": i},
{"inductive": {"index": i, "args": […]}}, "opaque"; returns è {"value": t},
{"io": t}, {"eio": {"error": e, "value": v}} oppure
{"async": {"op": i, "rets": […], "value": v}}. Il loro significato, e la codifica dei
valori a quei tipi, è il formato di trasmissione.
GenerateResponse
| Campo | Significato |
|---|---|
files |
I file del pacchetto: percorsi separati da /, relativi alla directory di output, mappati sui contenuti (testo). I percorsi non devono essere assoluti né contenere ... |
errors |
Perché la generazione è fallita. Quando non è vuoto, files viene ignorato. |
La directory di output viene sostituita esattamente dai file della risposta e da quelli di
lungo: build-info.json e assurance.json. Una risposta con un file chiamato assurance.json
viene rifiutata (LNG0504): il documento spetta a lungo, lo stesso in ogni
output. Un plugin che non può essere eseguito, esce con un errore, scrive
qualcosa che non è una GenerateResponse, segnala errori o non genera alcun file fa fallire il
comando con LNG0504; non viene pubblicato nulla.