Come vedere che cosa lungo ha generato per una dichiarazione

Questa guida mostra come scoprire che cosa è diventata una dichiarazione Lean: il suo nome e la sua firma in Rust, l’output del compilatore Lean da cui proviene, ciò da cui dipende e ciò che ne è affermato e dimostrato.

Prepara la riga di comando

Installa il comando lungo. Legge la configurazione da lungo.toml nella directory corrente. Scrivine uno che corrisponda al tuo build.rs: il progetto Lake e, in [lean], [rust] e [assurance], le impostazioni che build.rs modifica (vedi configurazione). Per configure().export_module("Formal").compile_lean("lean"):

project = "lean"

[lean]
export-modules = ["Formal"]

Senza il file, passa il progetto Lake e le impostazioni come opzioni: --project lean --export-module Formal. Un build.rs che chiama soltanto compile_lean("lean") richiede solo --project lean.

Trova il nome Rust di un nome Lean

lungo mappings

stampa ogni mappatura (elementi, costruttori e campi), per esempio:

  {
    "lean_name": "Formal.Sess.isOpen",
    "kind": "field",
    "rust_path": "Sess.is_open",
    "renamed": true
  },

Lo stesso file viene generato come names.json nell’output della build.

Esamina una dichiarazione

lungo inspect Formal.step

mostra il suo tipo Lean, il modulo e il file sorgente; ciò che ne è dimostrato, in sezioni:

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 ==
    …

(Claims: i claim di cui è soggetto, con il loro stato; Trust: ciò da cui dipende il suo codice e di cui nessuna dimostrazione si fa garante; Assumptions: ciò che quei claim assumono dell’host; Facilities: le facility dell’host che chiama), poi la sua firma compilata e le funzioni ausiliarie che il compilatore di Lean ne ha derivato. Dato un teorema che è la prova di un claim, una specifica, un’assunzione o una facility, inspect descrive invece quel record.

Per vedere il codice:

lungo ir Formal.apply     # la forma compilata di Lean (Bridge IR)
lungo rust Formal.apply   # il Rust generato

Scopri come sono implementati gli extern

lungo externs

elenca ogni extern raggiunto dal programma, indicando se lo implementa il runtime di lungo, una definizione Lean @[export] oppure una delle tue funzioni rust_extern (ogni operazione di una facility è implementata dall’host: in Rust, dalla sua funzione rust_extern).

Vedi che cosa si afferma degli export

lungo assurance             # ogni export
lungo assurance Formal.step # uno solo

riporta, per ogni export, i suoi claim, i suoi problemi di fiducia, le assunzioni che fanno i suoi claim e le facility di cui ha bisogno, dopo una riga che nomina il programma e la sua provenienza (la versione di Lean, la versione di lungo, lo schema del documento). --format json stampa lo stesso in JSON, e --claim-kind, --facility, --assumption e --trust-issue selezionano gli export. Vedi il comando lungo per ogni opzione, e il documento di garanzia per ciò che porta ogni pacchetto.

Leggi i metadati in esecuzione

Il modulo generato porta le stesse informazioni per le dichiarazioni esportate:

let info = formal::__meta::declaration("Formal.apply").unwrap();
println!("{} is {} at {:?}", info.lean_name, info.rust_path, info.source_file);
let claims = formal::__meta::assurance().claims_about("Formal.step");

Vedi codice generato per ogni campo e file.