catsenior507/dsh-tool-strict-check

严格检查 · Strict Check

别再重读自己写的 diff 了。让编译器说它是错的。

一个 DeepSeek Harness 宿主插件,只加一个工具 strict_check —— 用真正的检查器
去验证代码和命令,而不是再多一个观点。

License: MIT
DeepSeek Harness plugin
version
node
stars

English · 简体中文

要解决的问题

一个自信地犯错的 agent,不会因为"再看一眼"就改对。改动是它写的,所以它同意这个改动。
再读一遍 diff,只会得到同样的结论加上更多字。

而真正浪费回合的那些失败,恰恰是机械上可判定的:文件不再能解析、宿主 shell
根本跑不了的语法结构、一个让证明变成空话的 sorry、三个文件之外的类型错误。
这些都不需要判断力。它们需要一个检查器。

它做什么

一个工具,四个 action,由便宜到昂贵。

| action | 跑什么 | "通过"意味着什么 |
| --- | --- | --- |
| status | 用 --version 探测每个检查器 | 这台机器上能检查什么、不能检查什么 |
| lean | lean --json,并把警告提升为错误 | Lean 内核接受了这份证明 |
| batch | py_compile、node --check、tsc --noEmit、PowerShell 解析器 | 这门语言自己的编译器接受了这些文件 |
| commands | 对 shell 文本做静态规则检查,从不执行 | 没有命中已知的宿主 shell 陷阱 |

Lean 这一层才是「严格」的那层

Lean 检查之所以值得存在,唯一的理由就是它能说不。这里有两件事让这一点成立,
而它们都和"显而易见的实现"相反:

sorry 必须让检查失败。 lean file.lean 对一个满是 sorry 的文件退出码是 0,
因为在 Lean 里"证明没写完"只是一条 warning。一个跑了 Lean 然后读退出码的检查器,
会把一个空定理报告成"已验证"。所以实际命令是:

lean --json -DwarningAsError=true -DmaxErrors=0 -DautoImplicit=false -E hasSorry spec.lean

- -E hasSorry 只提升"证明缺失"这一类,于是既能要求"不许有未完成的目标",
又不必要求"不许有任何警告"。这个 kind 确实叫 hasSorry,不是 sorry。
- -DmaxErrors=0 去掉默认的 100 条上限 —— 超过之后 Lean 会停止报告并退出,
那会把第 100 条之后的错误全部藏起来。
- -DautoImplicit=false 关掉一个在 Lean 里默认开启的坑:开着它时,
一个拼错的假设名会静默变成一个全新的全称量词变量,定理陈述的东西比它读起来更弱。

检查器本身必须可信。 2026 年 Lean 内核与运行时里被发现 8 个可靠性缺陷,
每一个都被用来让官方内核接受 False 的证明,它们在 4.33.1 里被修复。
一份被更旧工具链接受的证明不能作为任何证据,所以版本会对着这条下限检查、
并随每条结果一起打印;低于下限的工具链会把"通过"变成 unsafe-toolchain。

它对「没跑」这件事是诚实的

unavailable 这个结论意味着没有任何检查器运行过,什么都没有被证明。
它永远不会被当作"通过"返回。如果 tsc 不在,结果会说出来并附上它找过的路径;
如果解析到的 lean 是没配默认工具链的 elan shim,结果也会说出来,
而不是报一个编译器错误。

安装

本插件作为包安装进一个 dsh profile。dsh plugin 会在 profile 目录里转发给 pnpm,
所以 pnpm 接受的任何 spec 都可以用。

从 GitHub 安装（公开发布形式）
dsh plugin --profile web add github:catsenior507/dsh-tool-strict-check

本地检出安装（开发时用）
dsh plugin --profile web add /absolute/path/to/dsh-tool-strict-check

web 是自带 GUI 的 profile;可换成 headless、sdk、acp 或你自己的 profile 名。
Windows 上路径用正斜杠,或给路径加引号。

装完重启宿主,然后确认:

strict_check action=status

Lean 是可选的,加装方式如下

另外三层不依赖 Lean。status 会把 Lean 报成 missing,lean action 返回
unavailable —— 永远不会是"通过"。

1. elan,Lean 的版本管理器
Windows（安装器写入 %USERPROFILE%\.elan）:
Invoke-WebRequest https://elan.lean-lang.org/elan-init.ps1 -OutFile "$env:TEMP\elan-init.ps1"
& "$env:TEMP\elan-init.ps1" -NoPrompt 1 -DefaultToolchain none

2. 工具链。4.33.1 是下限,不是建议值 —— 理由见上。
& "$env:USERPROFILE\.elan\bin\elan.exe" toolchain install leanprover/lean4:v4.33.1

插件不需要任何配置就能找到 Lean:它先去 /toolchains/*/bin
找真正的编译器,找不到才回退到 PATH。这是刻意的 —— PATH 上的 elan shim
在跑过一次 elan default 之前会拒绝运行,而那个拒绝很容易被误读成"Lean 坏了"。
要钉住某个特定工具链,在插件行里设置 leanPath。

走代理? elan 通过 curl 下载,而 curl 会读 ~/.curlrc。
如果工具链下载卡在 0 字节而浏览器正常,把
proxy = "http://127.0.0.1:" 写进 %USERPROFILE%\.curlrc 再重试。

安装不会做的事

- 没有构建步骤 —— 发布的 JavaScript 就是源码;不会跑 prepare 脚本,不需要打包器。
- 没有依赖 —— dependencies 和 peerDependencies 都是空的。cordis 由宿主在运行时提供。
- 没有 mathlib —— 代价见下。

需要 Node.js 20 或更新版本。

它不做什么

平实地说,因为一个自我吹嘘的验证工具比没有更糟:

- 没有 mathlib。 核心 Init 和 Std 随工具链自带,所以 import Std 和 by decide
不需要项目、不需要网络、不需要约 10 GB 下载就能用。你失去的是 tactic 库:
没有 ring、norm_num、push_neg、field_simp。替代品是 grind、decide、
by_cases、simp、omega。
- 没有沙箱级复核。 lake check、comparator、nanoda 需要 Linux 命名空间(bwrap),
在 Windows 上完全跑不起来。leanchecker 复核的是内核已经检查过的东西,而且抓不到
sorry,包一层只是成本没有覆盖。Lean 4.35 预计会自带 lake check;
那才是接入的时机,不是现在。
- 不检查「陈述是否符合你的本意」。 内核验证的是"这份证明证明了这条定理"。
这条定理是不是你想要的,那是一个规格问题,这个工具不会假装自己能回答 ——
这也正是 commands action 会打印"一次干净的扫描是弱证据"而不是"OK"的原因。

配置

dsh plugin add 已经替你插入了插件行。要改默认值,编辑 profile 的
cordis.patch.yml 里那一行的 config:

- insert:
- id: tool-strict-check
name: '@dsh-external/dsh-tool-strict-check'
config:
leanPath: '/toolchains//bin/lean.exe'
projectDir: ''
timeoutMs: 120000

leanPath 优先于自动发现 —— 这就是钉住某一个工具链的方式。

开发

npm test        # 61 个测试；Lean 相关的会真的执行编译器

没有安全工具链时,Lean 集成测试是跳过而不是伪造。解析测试回放的是
从 Lean 4.33.1 录下来的 lean --json 真实输出,所以线格式一变它们就会失败 ——
包括"线上位置是 0-based、会被转成 1-based"这个细节。

| 文件 | 职责 |
| --- | --- |
| lib/runner.js | 可执行文件发现、带超时的进程执行、spawn 失败处理 |
| lib/parse.js | 检查器输出 → 归一化诊断 |
| lib/static.js | 可读判定的缺陷与策略违规 |
| lib/language.js | 第 0 层:语言自己的编译器 |
| lib/lean.js | 严格层:flag、版本下限、结论 |
| lib/tool.js | strict_check 工具 |
| lib/policy-surface.js | dsh-policy-strict-gate 消费的契约 |

许可

MIT