Configurazione

lungo si configura in due posti che descrivono le stesse impostazioni:

• lungo.toml, letto dal comando lungo, per ogni linguaggio di output;
• un lungo_build::Builder in un build.rs di Cargo, per l’output Rust (compile_lean(project) equivale a configure().compile_lean(project)).

Ogni impostazione ha un valore predefinito. Le chiavi sconosciute sono errori (LNG0107).

# lungo.toml
project = "lean"

[lean]
root-modules = ["Formal.Session"]
assurance-modules = ["Formal.Laws"]

[assurance]
require-claims = ["Formal.Session"]

[rust]
out-dir = "src/generated"
type-attributes = [
  { path = "Formal", attribute = "#[derive(serde::Serialize, serde::Deserialize)]" },
]
rust-externs = { host_log = "crate::host::log" }

[go]
out = "gen/formal"
options = { package = "formal" }

[plugins.kotlin]
out = "gen/kotlin"

// build.rs
fn main() -> lungo_build::Result<()> {
    lungo_build::configure()
        .root_module("Formal.Session")
        .assurance_module("Formal.Laws")
        .require_claims("Formal.Session")
        .type_attribute("Formal", "#[derive(serde::Serialize, serde::Deserialize)]")
        .rust_extern("host_log", "crate::host::log")
        .compile_lean("lean")
}

Il file

I percorsi nel file (project, out, out-dir, toolchain-dir) sono relativi alla directory del file. lungo tiene i file di lavoro in .lungo/ accanto al file; aggiungila a .gitignore.

Programma

Si impostano in [lean], oppure con i metodi del Builder:

Quali extern implementa l’host non è un’impostazione: li dichiara il codice Lean del programma, come operazioni di facility (@[lungo_facility] e @[lungo_operation]; vedi come chiamare codice dell’host da Lean). Ogni pacchetto generato chiede all’host ogni operazione di ogni facility dichiarata dai moduli collegati del programma. La chiave extern di un’operazione è il simbolo del suo @[extern "symbol"], oppure il nome della dichiarazione per le altre forme di extern.

Senza root_module, le radici sono ciò che compila lake build: i moduli radice di ogni target predefinito del pacchetto radice (defaultTargets in lakefile.toml, @[default_target] in lakefile.lean), che sono librerie Lean (le loro roots) o eseguibili Lean (il loro root). Un pacchetto senza target predefiniti richiede root_module (LNG0301).

Senza export ed export_module, vengono esportati i moduli radice e i loro sottomoduli. Da un modulo esportato si esportano le definizioni, tranne quelle private, interne (componenti con prefisso _), le istanze e i loro metodi, quelle generate dal compilatore (ricorsori, matcher, noConfusion, proiezioni, costruttori, ausiliari strutturali), i tipi di nodo sintattico (syntax, notation, macro) e le definizioni meta.

Politica di fiducia

Si impostano in [lean]:

deny_sorry e deny_axioms si applicano anche all’evidenza di ogni claim (il teorema che nomina): un claim dimostrato con sorry, o con un assioma che la politica nega, viene rifiutato come lo sarebbe un export. Con deny-sorry = false, un tale claim viene riportato con stato incomplete, e non conta come claim dimostrato per require-claims.

Le violazioni fanno fallire la build con LNG0601.

Politica di garanzia

Si impostano in [assurance], oppure con i metodi del Builder. lungo controlla prima i record di garanzia del programma (la loro forma, le dichiarazioni che nominano, la forma di ogni claim); un problema in uno di essi fa fallire la build qualunque sia la politica, con un codice proprio (LNG0701–LNG0710). Poi:

Un percorso che non seleziona alcun export, o un nome che non è né un’assunzione né una facility del programma, è un errore (LNG0107): non potrebbe avere alcun effetto.

La politica fa parte di ciò da cui un output viene generato: renderla più stringente fa sì che lungo generate controlli di nuovo un output invece di considerarlo aggiornato.

Worker

Si impostano in [lean]:

Toolchain

Si impostano in [lean]:

Rust

Si impostano in [rust], oppure con i metodi del Builder:

Uno script di build può compilare più progetti Lean; ciascuno genera il proprio modulo, e due che genererebbero lo stesso modulo sono un errore (LNG0107). Dai a uno dei due un altro name.

Modellare il codice generato

Queste impostazioni selezionano elementi generati tramite un percorso. Il percorso . seleziona ogni elemento; qualsiasi altro percorso seleziona il nome Lean che compone e ogni nome al suo interno inteso come namespace: Formal seleziona Formal.Sess e Formal.Sess.isOpen, ma Formal.Se non seleziona nessuno dei due. I campi si indicano come in names.json: <Structure>.<field>, <Constructor>.<binder> oppure <Constructor>#<index>. Un percorso diverso da . che non seleziona nulla è un errore (LNG0107): non può avere alcun effetto.

In TOML, le impostazioni degli attributi sono liste di tabelle { path, attribute }, skip-debug e disable-comments liste di percorsi, ed extern-types una tabella da tipo Lean a percorso Rust.

Gli attributi si scrivono come nel sorgente Rust, #[…], e vengono posti dopo le derivazioni generate da lungo (Clone, Debug, e PartialEq, Eq, Hash dove ogni campo le ha), quindi possono essere #[derive(…)] di altri trait o attributi di quelle derivazioni, come #[serde(…)]. La feature serde del crate lungo implementa serde per i tipi della facciata.

Un tipo extern implementa lungo::LeanType per il backend in uso, ha i parametri del tipo Lean e rappresenta i suoi valori come fa il tipo Lean; in pratica è il tipo che un’altra build di lungo ha generato per lo stesso tipo Lean. Non viene generato, e i tipi che lo contengono derivano solo Clone e Debug. Implementa anche lungo::LeanLayout con l’impronta del layout del tipo Lean, che il modulo generato controlla quando viene compilato (vedi tipi extern); un tipo generato da lungo la implementa già. Vedi Come condividere tipi tra progetti Lean.

Opzioni dei generatori

La tabella di un linguaggio contiene la sua directory di output, out, e le sue opzioni, options, una tabella di stringhe. --<language>_opt=KEY=VALUE dalla riga di comando le integra (e le sostituisce). Un generatore rifiuta le opzioni che non conosce.

Go è sempre un pacchetto del modulo dell’host; non ha embed. Vedi pacchetti generati per ciò che scrive ciascun generatore.

Tipi extern

Un programma costruito sul modello di un altro programma (un pacchetto Lake che ne richiede un altro) usa i tipi di quel programma. Generati separatamente, ogni pacchetto avrebbe il proprio tipo per essi, e un valore dell’uno non potrebbe essere passato all’altro. La tabella extern-types di un linguaggio indica, per un tipo Lean, il tipo dell’altro pacchetto generato da usare al suo posto:

[go.extern-types."TaggedUrn.Exec.Wf"]
package = "github.com/machinefabric/tagged-urn-go/formal"   # ciò che un import indica
name = "Wf"                                                 # il tipo, come lo ha chiamato quel generatore

Il tipo deve essere usato dalle funzioni o dalle operazioni delle facility del programma (LNG0107 altrimenti). I valori passano allora tra i due pacchetti così come sono: i dati per valore, e i valori tenuti tramite handle come lo stesso handle, poiché ogni pacchetto di un processo gira sull’unico runtime.

In TypeScript ogni programma gira in una propria istanza WebAssembly, con una propria tabella di handle, quindi possono essere tipi extern solo i tipi i cui valori sono dati; un tipo i cui valori contengono un handle (un tipo opaco, una funzione) viene rifiutato indicandone il motivo.

Entrambi i pacchetti devono essere stati generati dalla stessa definizione del tipo, altrimenti un programma leggerebbe i valori dell’altro con il layout sbagliato. Ogni tipo generato porta l’impronta del suo layout (un digest dei suoi costruttori, dei loro campi e di ogni tipo che raggiungono, insieme alla versione di Lean), e un pacchetto che usa un tipo extern controlla quella del pacchetto che lo fornisce prima che qualcosa venga eseguito: in fase di compilazione in Rust, al caricamento del pacchetto in Go (init), Python (import), Swift e C (il primo uso del programma), e in TypeScript (la valutazione del modulo). Una discrepanza indica il tipo e il pacchetto; rigenerali entrambi dalla stessa definizione Lean.

Variabili d’ambiente

Punti di ingresso