This guide shows how to find out what a Lean declaration became: its Rust name and signature, the Lean compiler output it came from, what it depends on, and what is claimed and proved of it.
Set up the command line
Install the lungo command. It reads the configuration from
lungo.toml in the current directory. Write one that matches your build.rs: the Lake
project, and in [lean], [rust] and [assurance] the settings build.rs changes (see
configuration). For
configure().export_module("Formal").compile_lean("lean"):
project = "lean"
[lean]
export-modules = ["Formal"]
Without the file, pass the Lake project and settings as options:
--project lean --export-module Formal. A build.rs that only calls
compile_lean("lean") needs only --project lean.
Find the Rust name of a Lean name
lungo mappings
prints every mapping (items, constructors and fields), for example:
{
"lean_name": "Formal.Sess.isOpen",
"kind": "field",
"rust_path": "Sess.is_open",
"renamed": true
},
The same file is generated as names.json in the build output.
Inspect one declaration
lungo inspect Formal.step
shows its Lean type, module and source file; what is proved of it, in sections:
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: the claims it is the subject of, with their status; Trust: what its code depends
on that no proof vouches for; Assumptions: what those claims assume of the host;
Facilities: the host facilities it calls), then its compiled signature and the compiler
auxiliaries Lean derived from it. Given a theorem that is the evidence of a claim, a
specification, an assumption or a facility, inspect describes that record instead.
To see the code:
lungo ir Formal.apply # Lean's compiled form (Bridge IR)
lungo rust Formal.apply # the generated Rust
Find out how externs are implemented
lungo externs
lists every extern the program reaches, with whether the lungo runtime, a Lean
@[export] definition, or one of your rust_extern functions implements it (each operation
of a facility is implemented by the host: in Rust, by its rust_extern function).
See what is claimed of the exports
lungo assurance # every export
lungo assurance Formal.step # one
reports, for each export, its claims, its trust issues, the assumptions its claims make and
the facilities it needs, after a line naming the program and its provenance (the Lean
version, the lungo version, the schema of the document). --format json prints the same as
JSON, and --claim-kind, --facility, --assumption and --trust-issue select exports. See
the lungo command for every option, and
the assurance document for what every package carries.
Read the metadata at run time
The generated module carries the same information for exported declarations:
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");
See generated code for every field and file.