compiler_checks_report_json
The definition maps an input source string to a JSON report encoding the outcome of compiler checks. LNAL verification workflows cite it to standardize certificate output for downstream tooling. It proceeds by direct composition: extract the certificate via fromSource then serialize its status flag and error list through the JSON builder.
claimDefine the map sending a source string $s$ to the pretty-printed JSON object whose fields record the boolean verification flag and the list of error strings obtained from the compiler-check certificate of $s$.
background
CompilerChecksCert is a structure carrying a boolean ok flag together with a list of error strings; its verified predicate holds exactly when the flag is true. The companion mkJson function assembles these two values into a Lean.Json object with keys 'ok' and 'errors' and returns its pretty-printed string form. The surrounding LNALReports module supplies adapter functions that convert LNAL compiler artifacts into report strings for the URC layer.
proof idea
One-line wrapper that applies CompilerChecksCert.fromSource to the input string and immediately feeds the resulting ok and errors fields to mkJson.
why it matters in Recognition Science
The definition supplies the JSON export surface for compiler-check certificates inside the LNAL reporting pipeline. It completes the adapter path from certificate generation to machine-readable output, supporting the broader URC verification stack even though no downstream theorems currently reference it. The construction aligns with the framework's emphasis on explicit, auditable interfaces between formal certificates and external tooling.
scope and limits
- Does not execute any compiler passes or syntax validation.
- Does not interpret or filter the error list beyond direct serialization.
- Does not guarantee that the output JSON satisfies external schema standards.
- Does not handle exceptions or malformed source strings.
formal statement (Lean)
85def compiler_checks_report_json (src : String) : String :=
proof body
Definition body.
86 let cert := CompilerChecksCert.fromSource src
87 mkJson cert.ok cert.errors
88