compiler_checks_report_json
plain-language theorem explainer
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.
Claim. Define 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.