Il comando lungo

lungo genera codice da un programma Lean come protoc fa dai file .proto: un comando, una directory di output per linguaggio e plugin per altri linguaggi.

lungo [OPTIONS] <COMMAND>
lungo generate --c_out=gen/c --go_out=gen/go --python_out=gen/py --rust_out=gen/rust

Installazione

Con Homebrew, apt, dnf, Cargo o un download diretto per macOS, Linux e Windows: vedi installare lungo. Compilato da lungo-rs, lungo è una build di sviluppo (vedi il runtime).

Configurazione

La configurazione è lungo.toml nella directory corrente, un altro file indicato con --config, oppure il progetto Lake indicato con --project insieme alle impostazioni predefinite (vedi configurazione). Indicare sia un file sia --project è un errore.

Queste opzioni sono globali: possono precedere o seguire il comando.

generate

lungo generate [--<language>_out=DIR]... [--<language>_opt=KEY=VALUE[,KEY=VALUE]...]... [--runtime-dir DIR] [--wasi-sdk DIR] [--verify | --link]

Pacchetti generati descrive il pacchetto di ciascun linguaggio. Le DIR sulla riga di comando sono relative alla directory corrente; le directory out della configurazione al file di configurazione. Senza alcun --<language>_out, generate scrive gli output indicati dalla configurazione (ogni tabella di linguaggio con out, e [rust] con out-dir); se non ce n’è nessuno, fallisce (LNG0107). --<language>_opt aggiunge opzioni alle options del linguaggio e le sostituisce; rust non ha opzioni sulla riga di comando (le sue impostazioni sono tipizzate: vedi configurazione).

Ogni directory di output appartiene a lungo: viene sostituita per intero, e una directory che lungo non ha creato (una senza il suo build-info.json) non viene mai sostituita (LNG0107). Un output i cui input (il progetto Lean, la toolchain, lungo, il generatore e le sue opzioni, le politiche di fiducia e di garanzia) sono invariati, e che contiene ancora esattamente i file che ha generato (nessuno modificato, rimosso o aggiunto da allora), viene riutilizzato: generate stampa up to date: <language> <DIR> invece di generated <language> into <DIR>. Il progetto viene analizzato una volta per tutti gli output (una volta in più per ts, il cui target è WebAssembly a 32 bit).

Il codice generato spesso viene messo sotto commit, così gli utenti di un pacchetto non hanno bisogno né di Lean né di lungo. --verify controlla che sia aggiornato: genera ogni output senza scrivere, confronta con esso i sorgenti generati di ciascuna directory, stampa verified: <language> <DIR> per ciascuna che corrisponde, e fallisce con LNG0110 indicando ogni file modificato, mancante o in più. Non vengono confrontati né build-info.json né i prodotti di piattaforma.

Un prodotto di piattaforma è un file che un output collega per la macchina che lo scrive: il program.wasm del binding TypeScript, il programma collegato con il runtime WebAssembly. Funziona su ogni piattaforma, ma i suoi byte dipendono dalla macchina che ha compilato il runtime che collega, quindi due macchine collegano moduli diversi dagli stessi sorgenti. È un prodotto della build: generato insieme ai sorgenti, mai messo sotto commit (va ignorato dal controllo di versione; npm lo include dai files del pacchetto). --link scrive solo i prodotti di piattaforma, per questa macchina, negli output i cui sorgenti sono aggiornati — linked: <language> <DIR> for this machine — lasciando i sorgenti come sono; dove non lo sono non collega nulla e fallisce con LNG0110. Un checkout esegue --link prima di testare il binding TypeScript.

assurance

lungo assurance [DECLARATION] [--format human|json] [--claim-kind RELATION]... [--facility NAME]...
                [--assumption NAME]... [--trust-issue ISSUE]... [--policy] [--compose FILE]...

Riporta, export per export, ciò che il codice Lean del programma afferma e dimostra di esso, ciò che le sue dimostrazioni non coprono (la sua fiducia) e ciò che i suoi claim assumono dell’host, tenendo separate le tre cose. Compila e analizza il progetto come check, e rifiuta un programma i cui record di garanzia non sono validi (LNG0701–LNG0710): un rapporto su di essi sarebbe fuorviante.

Il rapporto leggibile comincia con il programma e la sua provenienza (versione e commit di Lean, versione di lungo, schema di garanzia), poi un blocco per export, con le sezioni == Claims ==, == Trust ==, == Assumptions == e == Facilities ==; una sezione vuota riporta (none). Lo stato di un claim è scritto tra parentesi quadre, [proved] o [incomplete] (poggia su sorry), con la sua relazione, le specifiche di cui parla e le assunzioni su cui poggia. Un’assunzione è scritta [assumed] con ciò che afferma — la sua definizione quando è una definizione, altrimenti il suo tipo — e la sua facility:

    [assumed] Polyglot.ScalesMonotonically : ∀ (a b : Nat), a ≤ b → Polyglot.hostScale a ≤ Polyglot.hostScale b (of Polyglot.Scaler)

Un export asincrono è marcato (async). --format json stampa lo stesso come oggetto JSON: schema_version, program, provenance, exports (come in assurance.json), i claims che li riguardano, policy (le violazioni, con --policy) e composition (le discrepanze).

I filtri di tipo diverso devono corrispondere tutti; i valori di uno stesso tipo corrispondono se almeno uno corrisponde.

--compose controlla che pacchetti generati separatamente descrivano allo stesso modo ogni record che condividono (una specifica, un claim, una facility o un’assunzione, per nome Lean): dallo stesso pacchetto, con lo stesso fingerprint. Un record descritto diversamente — una specifica, o una definizione del workspace che usa, cambiata in un pacchetto e non rigenerata nell’altro — viene riportato come LNG0708 con il pacchetto e il fingerprint di ciascun documento. Con una configurazione (un lungo.toml, --config o --project), il documento del progetto stesso è uno di quelli confrontati; senza, i file dati vengono confrontati tra loro, e ne servono almeno due. Un file che non è un documento di garanzia leggibile da lungo è LNG0711.

Il runtime

Ogni linguaggio esegue il programma sullo stesso runtime, precompilato per ogni piattaforma e pubblicato con ogni release di lungo: i pacchetti generati si riferiscono agli archivi del runtime della release tramite URL e digest SHA-256 (il CMake del pacchetto C lo scarica e lo controlla; le librerie di supporto di Go, Python, Swift e TypeScript lo contengono). Una release di lungo conosce la release del suo runtime dal manifest incorporato.

Una build di sviluppo di lungo (compilata dai sorgenti) non conosce alcuna release. Generare un pacchetto diverso da Rust richiede allora una distribuzione locale: una directory organizzata come una release (runtime/, wasm/, go/, python/, lungo-swift/, ts/), costruita da lungo-rs con cargo run -p lungo-dist -- local --out DIR e indicata con --runtime-dir DIR. Con --python PATH contiene anche la wheel di lungo-py per questa macchina in wheels/, perché pip la trovi (--find-links DIR/wheels) quando compila un pacchetto Python generato. Senza di essa il comando fallisce con LNG0108. I pacchetti generati si riferiscono allora a quella directory, quindi si compilano solo su quella macchina.

lungo runtime fetch [--target TRIPLE]
lungo runtime path [--target TRIPLE]
lungo runtime verify [--target TRIPLE]

Un download il cui digest differisce da quello della release viene scartato e segnalato come LNG0109. Il pacchetto del runtime contiene include/lungo.h, le librerie statiche e condivise in lib/, lib/cmake/lungo/lungoConfig.cmake e lib/pkgconfig/lungo.pc.

Aggiornamento

lungo self update

Sostituisce questo lungo con l’ultima release del canale su cui è stato pubblicato, e stampa lungo <vecchia> -> <nuova>, oppure lungo <versione> is the latest release quando non c’è nulla di più recente. Legge il manifest delle release del registro in cui questo lungo è stato pubblicato (quello indicato in installare lungo) e installa una release solo quando valgono tutte queste condizioni:

• la firma del manifest risale alle chiavi incorporate in questo lungo: un certificato per la chiave di release, firmato da due di quelle chiavi, valido in questo momento, e il manifest firmato da quella chiave di release;
• l’archivio ha la dimensione e il digest SHA-256 elencati nel manifest;
• il comando contenuto nell’archivio si avvia e dichiara la versione con cui è stato pubblicato.

Ogni altro caso è LNG0112, e il comando installato resta com’è. Il nuovo comando prende il posto del vecchio in un solo passo, là dove si trova il vecchio, quindi da quel momento il lungo nel tuo PATH è la nuova release. Su Windows il comando in esecuzione non può essere rimosso: resta accanto a quello nuovo come lungo.exe.old, e l’aggiornamento successivo lo rimuove.

Due tipi di lungo non si aggiornano in questo modo, e dicono che cosa li aggiorna (LNG0111):

Il lungo di un gestore di pacchetti si riconosce dal file installed-by che il suo pacchetto mette accanto al comando. Un lungo installato dove non puoi scrivere — /usr/local/bin, con sudo install — si aggiorna con gli stessi diritti: sudo lungo self update.

Altri comandi

Gli errori vengono stampati come error[LNGxxxx]: … (vedi errori) e il comando esce con stato 1 (assurance ha altri due stati: vedi sopra).

Esempio

$ lungo generate --go_out=gen/formal --python_out=gen/py
generated go into gen/formal
generated python into gen/py
$ lungo inspect Formal.step
Formal.step : Formal.Sess → Formal.Op → Bool × Formal.Sess
module: Formal.Session
source: lean/Formal/Session.lean
exported: yes
  == Claims ==
    [proved] lungo.preserves Formal.step_implements (of Formal.Spec)
  == Trust ==
    (none)
  == Assumptions ==
    (none)
  == Facilities ==
    (none)
  == Trust, in full ==
    axioms: (none)
    depends on sorry: false
    unsafe dependencies: (none)
    partial dependencies: (none)
    extern dependencies: lean_nat_add
compiled: (obj, u8) -> obj in module Formal.Session
compiler auxiliaries: Formal.step._boxed