{"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.2 修复（2026-10-13）：\n#   (a) v1.1.0 的 `lake build <t> --warning-as-error=error` 不是合法 lake 选项\n#       （实测：error: unknown long option '--warning-as-error'）。\n#   (b) target 语义修正：lake 的 build target 是模块名（Foo.Bar），不是文件路径；\n#       输入为 `X/Y.lean` 形式时自动翻译为 `X.Y`（要求文件位于包 src 根；若工程\n#       使用非标准 srcDir，请直接传模块名）。\n#   (c) v1.1.0 的 `metabot <pin> --download` 在 metabot CLI 中不存在（实测）。\n#       改为 metafile-indexer content URL 下载，支持 zip / tar.gz / tgz / git-bundle。\n#   (d) v1.1.1 采用的 `-KwarningAsError=true` 在 lean v4.12.0 实测**不升级** sorry\n#       警告（受控对照：sorry 向量在 -K 下 pass、在 --wfail 下 fail）——本版改用\n#       `lake --wfail`，自测 good→pass / bad→fail 通过（v4.12.0）。\n# 其余语义同前版：null/缺字段 → invalid；附件获取失败 → invalid，不猜测；\n# 构建退出码 0 = pass。\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\"\ncase \"$target\" in\n  *.lean) module=\"$(printf '%s' \"${target%.lean}\" | tr '/' '.')\" ;;\nesac\n\nif (cd \"$workdir\" && lake --wfail build \"$module\" >/dev/null 2>&1); then\n  printf '{\"verdict\":\"pass\",\"detail\":\"lake --wfail build %s clean\"}\\n' \"$module\"\nelse\n  printf '{\"verdict\":\"fail\",\"detail\":\"lake --wfail build %s failed (or contains sorry/admitted)\"}\\n' \"$module\"\nfi","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); file-path form X/Y.lean is auto-translated to module X.Y (file must live at package src root)\"}, \"nodeParams\": [\"target\"], \"stdin\": \"one JSON object\"}","output":"{\"detail\": \"string; `lake --wfail build <module>` outcome\", \"stdout\": \"one JSON object\", \"verdict\": \"pass | fail | invalid\"}","validation":{"enumeration_closure":{"closure":"the transitive import closure of the target module inside the pinned lake project, compiled by lake with warnings upgraded to failures (--wfail), so the verdict is a function of the complete set of compiler errors and sorry/admitted warnings — not of a subset","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, verdict pass confirmed"},{"expected_count":1,"expected_verdict":"fail","vector":"same project with `theorem t : True := by sorry` — executed 2026-10-13, verdict fail confirmed; note -KwarningAsError=true does NOT upgrade sorry warnings on v4.12.0 (controlled orthogonal test: bad vector passes under -K), hence --wfail"}]},"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-T3-JSP-000870","artifactPin":"metafile://028e1432d1059070fc76ceeed018c45429d1263ba5c2f0ad1c5e6e69c8dfb01ci0.json","correspondence":"metafile://028e1432d1059070fc76ceeed018c45429d1263ba5c2f0ad1c5e6e69c8dfb01ci0.json","coverage":["statement","definitions","proof-direction"],"note":"Independent correspondence artifact: wave1-correspondence-artifacts.json#correspondence-T3-JSP-000870 (unchanged since v1.1.0). A self-declared boolean is non-compliant; reviewers point semantic_check at this artifact."}}}