In questa sezione

Questa guida mostra come verificare che due o più pacchetti generati da lungo concordino su ciò che condividono, così che un claim che un pacchetto dimostra rispetto alla specifica di un altro pacchetto significhi ancora ciò che significava quando è stato dimostrato.

Perché la composizione va verificata

Un claim può citare una specifica di un altro pacchetto Lake. Nell’esempio semantic-model (lungo-rs/examples/semantic-model), il programma inventory dimostra che le sue ricerche costano quanto consente il modello di Acme Acme.Linear, e il pacchetto di Acme viene generato e distribuito separatamente:

inventory  ──afferma rispetto a──▶  Acme.Linear  ◀──dichiara──  acme

Ogni pacchetto porta il proprio assurance.json, generato dai sorgenti Lean da cui è stato costruito. Se Acme in seguito cambia Linear, un nuovo pacchetto Acme e il vecchio pacchetto inventory menzionano entrambi Acme.Linear, ma non intendono più la stessa cosa. Il claim dell’inventario è stato dimostrato rispetto alla vecchia definizione. Nessuno dei due pacchetti è sbagliato da solo; solo confrontarli lo rivela.

Che cosa viene confrontato

Ogni specifica, claim, facility e assunzione in un documento di garanzia ha un name, il package che la dichiara, e un fingerprint: lo SHA-256 di un testo canonico della sua dichiarazione Lean, di ogni definizione dei pacchetti del workspace Lake che usa, transitivamente, e della versione di Lean che l’ha elaborata.

Record Il suo testo comprende
Specifica il suo tipo e, per una definizione, il suo valore
Claim il suo enunciato, i suoi soggetti e le sue specifiche
Facility il suo tipo e, per una facility asincrona, i tipi delle sue operazioni
Assunzione il suo tipo e, per una definizione, il suo valore

Il testo canonico non contiene nomi di variabili legate né posizioni nel sorgente, quindi riformattare o rinominare una variabile legata non cambia un fingerprint; cambiare ciò che una dichiarazione dice sì. Lo cambia anche modificare qualunque cosa usi che sia dichiarata da un pacchetto del workspace: Acme.Linear si riduce ad Acme.CostBound, quindi cambiare Acme.CostBound cambia anche il fingerprint di Acme.Linear, e la composizione lo riporta. Le definizioni di Lean stesso sono coperte invece dalla versione di Lean. Come si calcola ogni fingerprint è in assurance.json.

La composizione prende ogni record descritto da almeno due documenti, per tipo e nome, e richiede che tutti diano lo stesso pacchetto e lo stesso fingerprint. I record presenti in un solo documento non vengono confrontati.

Componi i documenti

Passa ogni documento con --compose:

lungo assurance --compose gen/inventory/assurance.json --compose gen/acme/assurance.json
composition: 2 documents agree on every record they share

Quando un record differisce, lungo lo segnala come LNG0708 con ciò che dice ciascun documento, ed esce con stato 3:

error[LNG0708]: the specification Acme.Linear is described differently:
  gen/inventory/assurance.json: package acme, fingerprint 3c1e…
  gen/acme/assurance.json: package acme, fingerprint 9b70…

Un documento che lungo non riesce a leggere, o di una versione di schema che non legge, è LNG0711 (stato di uscita 1).

Eseguito fuori da un progetto (senza --config né --project, e senza lungo.toml nella directory corrente), lungo assurance --compose confronta soltanto i documenti che riceve, e ne richiede almeno due.

Componi rispetto al progetto

Dentro un progetto, il documento del progetto stesso, costruito dai sorgenti Lean così come sono ora, viene confrontato con ogni documento dato:

cd examples/semantic-model
lungo assurance --compose vendor/acme/assurance.json

Il rapporto sugli export del progetto viene stampato come al solito, seguito dal risultato della composizione. Con --format json, le discrepanze sono elencate sotto composition nel rapporto. --policy e --compose si possono combinare: una violazione della politica esce con stato 2 e ha la precedenza su una discrepanza di composizione (stato 3).

Verificalo in CI

Componi i documenti di tutti i pacchetti che distribuisci insieme, e fallisci su uno stato diverso da zero:

lungo generate --go_out=gen/inventory
lungo --config acme/lungo.toml generate --go_out=gen/acme
lungo assurance --compose gen/inventory/assurance.json --compose gen/acme/assurance.json

Entrambi i documenti devono provenire dalla stessa versione di Lean: la versione fa parte di ogni fingerprint, quindi documenti costruiti con toolchain diverse discordano su ogni record che condividono.

Quando la verifica fallisce, rigenera i pacchetti dagli stessi sorgenti, poi verifica di nuovo i claim. Una specifica cambiata richiede di dimostrare di nuovo ogni claim che la cita, cosa che la build del pacchetto dipendente fa.

Vedi anche