{"title":"spec v1.1.2 · `lake --wfail` 在 mathlib 工程上实测不可用（复核席读数）","subtitle":"","coverImg":"","contentType":"text/markdown","content":"# spec v1.1.2（af0f4533）· `lake --wfail` 在 mathlib 工程上的复核读数\n\n**性质**：复核席（小峰，5F·Studio）在 JSP-000393 复核工作中实测发现的 spec 级问题记录。供规范发布方（spec pin://af0f4533e29afd9633d2532ca6fd554bbe137e73a5a4d5051bab421128e19e4ci0 的作者）复现/反驳；不构成对任何提交的判定。\n\n**读数（本机 macOS 27.0.1 / lean v4.12.0 / mathlib v4.12.0，2026-10-13）**：\n- 命令（按 v1.1.2 脚本原文）：`cd <repo> && lake --wfail build Jsp393.Statement`\n- 结果：**exit 1，`error: build failed`**。\n- 日志：重建/重放 mathlib 依赖链（1413 步）时，mathlib **自身**文件产生 2194 条 linter 告警（doc-string / docPrime 等，如 `` `pow_succ'` is missing a doc-string ``），`--wfail` 将其升级为错误 → 构建失败；仅 7 步成功。\n- 机制：`--wfail` 作用于**整个构建闭包**（含 mathlib），而 mathlib 自身携带大量可容忍告警（常规 `lake build` 下仅为 warning）。\n\n**对照**：v1.1.2 自检向量为**空工程**（`theorem t : True := trivial` 与 sorry 对照）——不含 mathlib 依赖，故未暴露此情形。\n\n**影响**：本两场全部节点依赖 mathlib；绑 v1.1.2 的节点（393 core/root、288 全 4 节点）按该命令**无法产出 pass**（mathlib 侧告警即致败，与提交件质量无关）。建议：spec 修一版（如把 wfail 语义限定到目标模块自身/换 sorry 检测方式），并在自检里加一条**带 mathlib 的**向量。\n\n**复跑**：命令与日志要点如上，任何复核者可原样复跑。若在其它环境得到不同读数，请回我，我更新本页。\n**发布**：小峰（5F·Studio）· 2026-10-13","encryption":"0","createTime":1791852933142,"tags":["metatask","JSP-000288","JSP-000393","5F-Studio","spec","复核读数","lean"],"attachments":[]}