{"name":"lean-build","lang":"bash","entry":"spec-lean-build.sh","script":"#!/usr/bin/env bash\n# spec-lean-build.sh — 通用 Lean 形式化验证器（MetaTask spec 脚本，协议 v1.2.1 §spec 契约）\n#\n# 输入（stdin，JSON）: { \"repo\": \"pin://|metafile://|本地路径\", \"target\": \"相对于 repo 根的 .lean 文件\" }\n# 输出（stdout，JSON）: { \"verdict\": \"pass\" | \"fail\" | \"invalid\", \"detail\": \"...\" }\n# 判据: 在仓库根执行 lake build <target>，退出码 0 = pass（全部定理无 sorry 报错即视为\n#       编译判定；--warning-as-error=error 保证 sorry/lint 失败即失败）。\n# null/缺失 → invalid 并注明位置（协议 null_tolerance 判据）。\n# 离线性: 输入为 pin://|metafile:// 时先经 metaid 内容端点拉取（发射环境自带工具）；\n#         拉取失败 → invalid，不悬挂。\nset -euo pipefail\n\ninput=\"$(cat)\"\n\nrepo=\"$(printf '%s' \"$input\" | python3 -c 'import json,sys; d=sys.stdin.read(); print(json.loads(d).get(\"repo\") or \"\")' 2>/dev/null || true)\"\ntarget=\"$(printf '%s' \"$input\" | python3 -c 'import json,sys; d=sys.stdin.read(); print(json.loads(d).get(\"target\") or \"\")' 2>/dev/null || true)\"\n\ninvalid() { printf '{\"verdict\":\"invalid\",\"detail\":\"%s\"}\\n' \"$1\"; exit 0; }\n[ -n \"$repo\" ] || invalid \"missing field: repo\"\n[ -n \"$target\" ] || invalid \"missing field: target\"\n\nworkdir=\"$repo\"\ncase \"$repo\" in\n  pin://*|metafile://*)\n    tmp=\"$(mktemp -d)\"\n    if ! fetch_output=\"$(metabot \"$repo\" --download \"$tmp\" 2>&1)\"; then\n      invalid \"artifact fetch failed: $fetch_output\"\n    fi\n    workdir=\"$tmp\"\n    ;;\nesac\n\n[ -f \"$workdir/lakefile.lean\" ] || [ -f \"$workdir/lakefile.toml\" ] || invalid \"not a lake project root: $workdir\"\n\nif (cd \"$workdir\" && lake build \"$target\" --warning-as-error=error >/dev/null 2>&1); then\n  printf '{\"verdict\":\"pass\",\"detail\":\"lake build %s clean\"}\\n' \"$target\"\nelse\n  printf '{\"verdict\":\"fail\",\"detail\":\"lake build %s failed (or contains sorry/admitted)\"}\\n' \"$target\"\nfi\n","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":{"detail":"string; `lake build <target> --warning-as-error=error` outcome","stdout":"one JSON object","verdict":"pass | fail | invalid"},"validation":{"enumeration_closure":{"closure":"the transitive import closure of the target .lean file inside the pinned repo, compiled by lake with --warning-as-error=error; the verdict is a function of the complete set of compiler errors and sorry/admitted warnings","count_meaning":"numbers of build-failing declarations (errors + sorry warnings) in each vector","expected_count":1,"selfcheck":[{"expected_count":0,"expected_verdict":"pass","vector":"empty lake project, target = `theorem t : True := trivial`"},{"expected_count":1,"expected_verdict":"fail","vector":"same project with `theorem t : True := by sorry`"}]},"note":"Protocol v1.2.1 paths.spec.fields.validation (verbatim): H_ACT2 及以后发布的 spec 必填且三项齐备——null_tolerance（bool：任何分支把 null/缺失输入映射为 verdict=invalid 并在 detail 给出位置，未捕获异常判非合规）；enumeration_closure（object：声明闭包并附至少一个具体自检向量，期望计数须为整数字段供机械对账，如 n=8→28）；proposition_fidelity（object：必须引用独立 correspondence 件（pin://|metafile://）承载逐项对照表——定理陈述／定义／证明方向对齐原始命题；自报布尔判非合规；复核者经 semantic_check 指向该件）","null_tolerance":true,"proposition_fidelity":{"artifactKey":"correspondence-T4-JSP-000598","artifactPin":"metafile://278227d8e0c2190de8a40a17d15dde99dc6062bdfc75ec5dd0f7b7ef747e21b9i0.json","correspondence":"metafile://278227d8e0c2190de8a40a17d15dde99dc6062bdfc75ec5dd0f7b7ef747e21b9i0.json","coverage":["statement","definitions","proof-direction"],"note":"Independent correspondence artifact: wave1-correspondence-artifacts.json#correspondence-T4-JSP-000598. Publish it first and replace the placeholder with its pin://|metafile:// id in BOTH correspondence and artifactPin. A self-declared boolean is non-compliant (radical (set) reading of equal prime divisors is the item to recheck)."}}}