{"name":"jsp393-lean-statement-core","lang":"bash","entry":"spec-lean-build.sh","script":"pin://5a4c2e6057444afcdd83aaaec0c19782c97e8d8e9d87fb53b483c326e8c79151i0","input":{"fields":{"repo":"pin://|metafile:// artifact or local path of the lake project root","target":"path of the .lean file to build, relative to the repo root"},"nodeParams":["target"],"stdin":"one JSON object"},"output":{"verdict":"pass | fail | invalid","stdout":"one JSON object","detail":"lake build <target> outcome"},"validation":{"null_tolerance":true,"enumeration_closure":{"closure":"the transitive import closure of the node target .lean file inside the pinned repo, compiled by lake; the verdict is a function of the complete set of compiler errors and sorry/admitted warnings for that closure. This pin reuses the already-published lean-build verifier script rather than re-deriving it.","count_meaning":"harness self-checks executed for THIS pin before publish (0: no Lean toolchain on the publishing machine, so no new execution is claimed here)","selfCheckCount":0,"inheritedExecutions":"pin://5a4c2e6057444afcdd83aaaec0c19782c97e8d8e9d87fb53b483c326e8c79151i0"},"proposition_fidelity":{"artifact":"pin://bfccdbc259063bee4c9c5308ccdfb38004f1538860b85090a8c3f6a837f02553i0","note":"the correspondence pin records the official question verbatim, the live problem-bank status, the degraded formalization scope and the honesty clauses; the node targets and acceptance text follow that pin"}}}