ExportNative.lean

1 import ProofPath.Examples
2 import Lean
3 
4 open Lean Elab Command
5 
6 /-- Export actual compiled dependency metadata. This metaprogram is not itself
7     a formally verified parser or a general proof-term interpretation theorem. -/
8 elab "#export_native_field " file:str : command => do
9   let env ← getEnv
10   let roots : Array Name := #[
11     `ProofPath.Field.derives_iff_all_models,
12     `ProofPath.Field.support_cover_gluing,
13     `ProofPath.protected_alternative,
14     `ProofPath.exact_observation_count,
15     `ProofPath.all_predicates_sufficient_iff_injective]
16   let allowed := #[`propext, `Classical.choice, `Quot.sound]
17   let mut names : Array Name := roots
18   let mut justifications : Array Json := #[]
19   let mut records : Array Json := #[]
20   for root in roots do
21     let some info := env.find? root | throwError "missing declaration {root}"
22     let axioms ← collectAxioms root
23     for ax in axioms do
24       unless allowed.contains ax do
25         throwError "forbidden dependency {ax} in {root}"
26     let deps := info.getUsedConstantsAsSet.toArray.filter (· != root)
27     for dep in deps do
28       unless names.contains dep do names := names.push dep
29     let js := deps.map (fun d => Json.str d.toString)
30     justifications := justifications.push <| Json.mkObj [
31       ("id", toJson ("native:" ++ root.toString)),
32       ("premises", Json.arr js), ("conclusion", toJson root.toString),
33       ("rule", toJson "compiled Lean type and proof constant dependencies"),
34       ("certified", toJson true), ("evidence_ids", toJson #["lean-environment"])]
35     records := records.push <| Json.mkObj [
36       ("declaration", toJson root.toString),
37       ("axioms", toJson (axioms.map Name.toString)),
38       ("direct_dependencies", Json.arr js)]
39   let nodes := names.map fun n => Json.mkObj [
40     ("id", toJson n.toString), ("label", toJson ("Lean declaration: " ++ n.toString)),
41     ("kind", toJson (if roots.contains n then "theorem" else "external_result"))]
42   let payload := Json.mkObj [
43     ("schema_version", toJson "1.0"),
44     ("metadata", Json.mkObj [
45       ("scope", toJson "Syntactic dependencies of five compiled declarations. Nonselected dependencies are explicit external leaves. This export does not recover failed discovery routes."),
46       ("lean_version", toJson Lean.versionString), ("native_records", Json.arr records)]),
47     ("premises", toJson ((names.filter (!roots.contains ·)).map Name.toString)),
48     ("targets", toJson (roots.map Name.toString)), ("nodes", Json.arr nodes),
49     ("evidence", Json.arr #[Json.mkObj [
50       ("id", toJson "lean-environment"), ("kind", toJson "formal_proof"),
51       ("source", toJson "ExportNative.lean freshly imports the built ProofPath modules"),
52       ("scope", toJson "Already elaborated named declarations; transitive axiom allowlist checked"),
53       ("certifies", toJson true)]]),
54     ("justifications", Json.arr justifications)]
55   liftIO <| IO.FS.writeFile file.getString (payload.pretty ++ "\n")
56 
57 #export_native_field "../data/native_lean_field.json"

Back to source controls