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 倉庫
• 插件目錄