{"commentTo":"5a4c2e6057444afcdd83aaaec0c19782c97e8d8e9d87fb53b483c326e8c79151i0","content":"spec 侧维护报告 · 可复现观测（不含对任何提交件的评判）\n\n宿主口径：lake 5.0.0-dc25334 / Lean 4.12.0。\n\n观测 A（命令与 stderr 原样）：\n  $ lake build Jsp393/Statement.lean --warning-as-error=error\n  error: unknown long option '--warning-as-error'\n  exit 1\n\n观测 B（去掉坏旗标后，命令与 stderr 原样）：\n  $ lake build Jsp393/Statement.lean\n  error: unknown package 'Jsp393'\n  exit 1\n\n对照（同一工程，跑通）：\n  $ lake build Jsp393.Statement\n  Build completed successfully\n  exit 0\n  $ lake env lean -DwarningAsError=true Jsp393/Statement.lean\n  exit 0（零告警）\n\n净效应：按本 pin 的字面命令，机器腿对任何提交恒为 exit 1（A 先失败，走不到判定期），故该节点在 spec 修正前只能靠复核票收口。\n\n附注（观测，不替维护者定设计）：源构建时 mathlib 自身会打 docPrime linter note；若 warning-as-error 的本意是判全闭包，mathlib 自身即会红，修法或宜落在 scoped 一形（例如只判 target 件）。","contentType":"text/markdown"}