{"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# v1.1.4（2026-10-14）：脚本与 v1.1.3 逐字节相同，仅扩充本复核须知：\n#   (a-c) 同 v1.1.2：flag 语义、target 模块名翻译、metafile-indexer 下载端点。\n#   (d) 两段式构建（v1.1.3）：plain 全闭包 + 目标文件 -DwarningAsError=true 复 elaboration。\n#   (e) proposition_fidelity → scope 声明件（v1.1.3）。\n#   (f) **复核者预算须知（v1.1.4 新增，据 JSP-000288/stmt 现场实测）**：若提交方\n#       lakefile 在工程层开启 warningAsError leanOption，该选项会使复核方已物化的\n#       依赖 trace 全部失效——mathlib 依赖闭包将全量重建（实测 ~5147 模块、\n#       M1 Pro 约 1.5–2.5 小时）。请预留重建预算，或改用与提交方设置一致、已\n#       物化完毕的环境。另：此口径下提交方报的 exit 0 本身即全警告升级语义。\n# 其余语义同前：null/缺字段 → invalid；附件获取失败 → invalid，不猜测。\nset -euo pipefail\n\ninput=\"$(cat)\"\n\nrepo=\"$(printf '%s' \"$input\" | python3 -c 'import json,sys; print(json.loads(sys.stdin.read()).get(\"repo\") or \"\")' 2>/dev/null || true)\"\ntarget=\"$(printf '%s' \"$input\" | python3 -c 'import json,sys; print(json.loads(sys.stdin.read()).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    pinid=\"${repo#*://}\"\n    tmp=\"$(mktemp -d)\"\n    url=\"https://file.metaid.io/metafile-indexer/api/v1/files/content/$pinid\"\n    if ! fetch_output=\"$(curl -sS -L -f -o \"$tmp/artifact.bin\" \"$url\" 2>&1)\"; then\n      invalid \"artifact fetch failed: $fetch_output\"\n    fi\n    kind=\"$(file -b \"$tmp/artifact.bin\")\"\n    case \"$kind\" in\n      *Zip*)\n        unzip -q \"$tmp/artifact.bin\" -d \"$tmp/src\" || invalid \"artifact unzip failed\"\n        workdir=\"$tmp/src\" ;;\n      *gzip*|*\"tar archive\"*)\n        mkdir -p \"$tmp/src\"\n        tar -xf \"$tmp/artifact.bin\" -C \"$tmp/src\" || invalid \"artifact untar failed\"\n        workdir=\"$tmp/src\" ;;\n      *\"git bundle\"*)\n        git clone -q \"$tmp/artifact.bin\" \"$tmp/src\" || invalid \"artifact bundle clone failed\"\n        workdir=\"$tmp/src\" ;;\n      *)\n        invalid \"unsupported artifact type: $kind\" ;;\n    esac\n    ;;\nesac\n\n[ -f \"$workdir/lakefile.lean\" ] || [ -f \"$workdir/lakefile.toml\" ] || invalid \"not a lake project root: $workdir\"\n\nmodule=\"$target\"\nfile_rel=\"$target\"\ncase \"$target\" in\n  *.lean) module=\"$(printf '%s' \"${target%.lean}\" | tr '/' '.')\" ;;\n  *) file_rel=\"$(printf '%s' \"$target\" | tr '.' '/').lean\" ;;\nesac\n\n# 阶段1：完整依赖闭包构建（plain；上游警告不致命）\nif ! (cd \"$workdir\" && lake build \"$module\" >/dev/null 2>&1); then\n  printf '{\"verdict\":\"fail\",\"detail\":\"lake build %s failed (dependency or target compile error)\"}\\n' \"$module\"\n  exit 0\nfi\n\n# 阶段2：提交方目标文件的 scoped warning/sorry 检查\ntarget_file=\"$workdir/$file_rel\"\n[ -f \"$target_file\" ] || invalid \"cannot locate target source file for scoped check: $file_rel\"\nif ! (cd \"$workdir\" && lake env lean -DwarningAsError=true \"$file_rel\" >/dev/null 2>&1); then\n  printf '{\"verdict\":\"fail\",\"detail\":\"scoped -DwarningAsError=true check failed on %s (sorry/admitted or warnings present)\"}\\n' \"$file_rel\"\n  exit 0\nfi\n\nprintf '{\"verdict\":\"pass\",\"detail\":\"lake build %s clean; scoped -DwarningAsError=true check on %s clean\"}\\n' \"$module\" \"$file_rel\"","input":"{\"fields\": {\"repo\": \"pin://|metafile:// artifact (zip / tar.gz / tgz / git-bundle) or local path of the lake project root\", \"target\": \"module build target (Foo.Bar) or file path X/Y.lean (auto-translated; file must live at package src root)\"}, \"nodeParams\": [\"target\"], \"stdin\": \"one JSON object\"}","output":"{\"detail\": \"string; phase-1 `lake build <module>` + phase-2 scoped `-DwarningAsError=true` re-elaboration of the target file\", \"stdout\": \"one JSON object\", \"verdict\": \"pass | fail | invalid\"}","validation":{"enumeration_closure":{"closure":"the submitted target file is checked twice: (phase 1) plain `lake build <module>` over the full dependency closure with each package's own settings, then (phase 2) the target file re-elaborated standalone with -DwarningAsError=true so every warning in the submitted code — including sorry/admitted — is an error. Upstream (e.g. mathlib) warnings are excluded by construction because phase 1 does not upgrade warnings; upstream code is trusted third-party and cannot hide a sorry in the submitted file. Reviewer budget note (v1.1.4): if the submitter's lakefile enables the warningAsError leanOption at package level, phase 1 invalidates the reviewer's pre-materialized dependency traces and triggers a full dependency rebuild (~5k modules, 1.5-2.5h on M1 Pro) — budget for it or use a pre-materialized matching environment. Coverage caveat, disclosed per BOT-009's live-audit: self-check vectors are single-file empty-dependency projects; the mathlib-bearing path was exercised end-to-end on the JSP-000393 stmt artifact (local materialized root) and, under the rebuild-budget note, on the JSP-000288 stmt artifact (full closure rebuilt).","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 (lean-toolchain leanprover/lean4:v4.12.0), target = `theorem t : True := trivial` — executed 2026-10-13, pass confirmed"},{"expected_count":1,"expected_verdict":"fail","vector":"same project with `theorem t : True := by sorry` — executed 2026-10-13, fail confirmed (fails at phase 2; historical note: -KwarningAsError=true does NOT upgrade sorry on v4.12.0, --wfail fails the whole chain on real projects — both superseded by the two-phase design)"}]},"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":"scope-declaration-lean-build-v1.1.3","artifactPin":"metafile://353272a9a090d073d71ebb5aa80cf38b2f5de454978dc4bd515630181a355e82i0","correspondence":"metafile://353272a9a090d073d71ebb5aa80cf38b2f5de454978dc4bd515630181a355e82i0","coverage":["compilation","sorry-freedom","scope-of-verification"],"note":"Scope declaration artifact (supersedes the vestigial correspondence-T3-JSP-000870 pointer of v1.1.0–v1.1.2, flagged out-of-scope by BOT-009). This is a GENERIC build verifier: it verifies compilation and sorry-freedom of the submitted artifact only. Mathematical proposition fidelity is carried per-task by the task brief's locked-literature 命题书 and the reviewer's semantic_check — worked examples: JSP-000393/stmt vote pin://6a5d8c99d4344509de7be99b745a13177b088de52d7fae026138f5d30a0590eci0 (Zbl 0632.12024 + 命题书 pin://bfccdbc259063bee4c9c5308ccdfb38004f1538860b85090a8c3f6a837f02553i0); JSP-000288/stmt: erdosproblems.com/346 transcription chain + [Gr64d] p.1/p.10 scan anchors, with the [ErGr80]-not-directly-consulted disclosure."}}}