dsh-tool-strict-check: 用真实编译器校验代码与命令

在 DeepSeek Harness (DSH) 的开发流程中，智能体往往因为是自己编写的代码而“自信地犯错”。当它再次阅读自己的 diff 时，只会得到相同的答案，无法修复那些机械性错误——比如文件解析失败、Shell 构造无法运行、证明中存在 sorry 或者类型错误。这些错误不需要判断，只需要检查器。

dsh-tool-strict-check 是一个 DSH 主机插件，它引入了一个名为 strict_check 的工具，用真实的检查器（Lean 4 内核、语言编译器、Harness Shell 危险规则）来替代主观判断，验证代码和命令。该插件位于 admin-security 类别，由 catsenior507 维护，使用 MIT 许可证。

核心功能¶

该插件提供四种检查模式，按成本从低到高排列：

1. status：探测每个检查器是否可用。它会对每个检查器运行 --version，报告当前机器上哪些检查器可用，哪些不可用。
2. lean：运行 Lean 4 编译器。为了确保严格性，它将警告提升为错误，并使用特定的命令行参数来防止静默失败。这确保了 Lean 内核真正接受该证明。
3. batch：运行语言的编译器或解析器，包括 py_compile、node --check、tsc --noEmit 和 PowerShell 解析器。
4. commands：对 Shell 文本应用静态规则。这些规则不执行命令，仅检查文本模式，以防止已知的 Harness Shell 危险操作。

在 lean 模式中，插件会显式关闭默认的自动隐式参数（-DautoImplicit=false），并使用 -E hasSorry 专门检查未完成的证明。这确保了包含 sorry 的文件会被拒绝，而不是仅仅因为 Lean 将其视为警告而通过。

安装与启用¶

插件需要安装到 DSH 的一个 profile 中。安装命令如下：

# 从 GitHub 安装
dsh plugin --profile web add github:catsenior507/dsh-tool-strict-check

web 是 DSH 默认的 GUI profile，也可以替换为 headless、sdk 或其他自定义 profile。安装后需要重启 DSH 主机，并通过以下命令确认：

strict_check action=status

Lean 4 可选配置¶

batch 和 commands 模式不需要 Lean 4，但 lean 模式需要。如果仅使用其他模式，可以跳过 Lean 4 安装。

要启用 Lean 4 检查，需要安装 elan 版本管理器和指定工具链。插件要求 Lean 4.33.1 或更高版本，因为更早的版本存在内核健全性漏洞。

# 1. 安装 elan (Windows 示例)
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. 安装 Lean 4.33.1
& "$env:USERPROFILE\.elan\bin\elan.exe" toolchain install leanprover/lean4:v4.33.1

插件会自动查找 <ELAN_HOME>/toolchains/*/bin 下的真实编译器。如果需要锁定特定工具链，可以通过配置指定 leanPath。

配置¶

安装命令通常会在配置文件中插入插件行。如需修改默认行为，编辑对应 profile 的 cordis.patch.yml：

- insert:
    - id: tool-strict-check
      name: '@dsh-external/dsh-tool-strict-check'
      config:
        leanPath: '<ELAN_HOME>/toolchains/<toolchain>/bin/lean.exe'
        projectDir: '<path to a Lake project, if your specs import one>'
        timeoutMs: 120000

注意事项¶

该插件以当前 DSH 进程的权限运行，使用 pnpm 作为内部依赖管理工具。

需要注意的是，该插件目前不支持 mathlib。虽然核心库可以工作，但失去了 tactic 库（如 ring, norm_num 等）。此外，插件不提供沙盒化的重新检查，也不进行“语句 vs 意图”的检查。它仅验证代码是否符合语法和类型要求。

总结¶

dsh-tool-strict-check 旨在让编译器“说话”，通过强制执行真实的编译器规则来减少智能体在机械性错误上的浪费。它适合需要严谨代码验证的开发场景，但不承诺解决所有逻辑错误。

• GitHub 仓库
• 插件目录