怎样使用

如果你已经打开 http://127.0.0.1:3080/，并且当前 Web Profile 已加载本插件，那么不需要手动启动 Lean，也不需要填写工具 JSON。只需新建对话，给模型数学题，并明确要求它在完成前调用 lean_check。

可以先把下面这段测试要求交给模型。它只给出任务，不给出答案：

请使用 Lean 4 和 Mathlib 证明自然数加法满足：1 + 2 = 2 + 1。

要求：
1. 自行写出完整 Lean 4 源码；
2. 自行选择最小必要的 Mathlib 子模块，不要使用 import Mathlib；
3. 生成第一版代码后，必须调用 lean_check；
4. 若 lean_check 返回错误，请依据错误信息修改并继续验证；
5. 只有 lean_check 返回 verified 或 verified_with_warnings 后，才能说明证明完成。

第一次 lean_check 可能需要几十秒到数分钟：Lean LSP 需要把所需的、已经存在于本机的 .olean 文件读入内存。这不是下载或全量重编译 Mathlib。之后同一 Web 服务中的验证会复用常驻进程，结果里的 reusedProcess 通常为 true，速度会明显提升。

Harness 如何加载和使用插件

本插件不需要复制到 deepseek-harness 的 packages/ 目录。它作为一个 DSH Bundle 被 Profile 安装和加载：

deepseek-harness Web Profile
        │
        │  安装 lean4-harness-plugin
        ▼
package.json 的 dsh.bundle 声明
        │
        ▼
cordis.patch.yml
        │  插入 lean4-harness-plugin/dsh
        ▼
dsh-plugin.js（Cordis 入口，apply(ctx)）
        │
        ├── 注册 lean_check
        ├── 注册 lean_repl_request
        ├── 注册 lean_format_tactic_state
        ├── 注入 Lean 验证提示
        └── 阻止模型直接执行危险的 Lake / Mathlib 操作
        │
        ▼
dist/index.js
        │
        ▼
LeanReplService + LeanFormatter
        │
        ▼
lean/ Lake 工作区 ──── D:/mathlib4 的本地 .olean 缓存

因此，deepseek-harness 是宿主，而 D:\lean4-harness-plugin 是 Lean 验证逻辑的唯一来源。以后修改插件时，只需重新构建本仓库并重启 Harness，不必在 Harness 源码中维护第二份 Lean 实现。

Bundle 配置

默认配置位于 cordis.patch.yml：

- insert:
    - id: lean4-harness-plugin
      name: 'lean4-harness-plugin/dsh'
      config:
        mathlibRoot: 'D:/mathlib4'
        requestTimeoutMs: 600000
        buildTimeoutMs: 600000
        prewarm: false
        prewarmSource: |
          import Mathlib.Data.Nat.Basic

字段	默认值	作用
`workspaceRoot`	插件包内的 `lean/`	Lake 工作区路径。
`mathlibRoot`	`D:/mathlib4`	Mathlib 写入防护范围；不替代 `lakefile.lean` 的依赖路径。
`lakeCommand`	`lake`	Lake 命令或绝对路径。
`leanCommand`	`lean`	Lean 命令或绝对路径。
`requestTimeoutMs`	`600000`	前台启动、验证和诊断最大时长，单位毫秒。
`buildTimeoutMs`	`600000`	已授权精确模块构建最大时长，单位毫秒。
`prewarm`	`false`	`true` 时 Web 启动后预热可信导入；`false` 时首个 `lean_check` 延迟启动。
`prewarmTimeoutMs`	`90000`	后台预热最大时长，单位毫秒。
`prewarmSource`	`import Mathlib.Data.Nat.Basic`	预热使用的可信源码。
`maxResultChars`	`16000`	返回给模型的 stderr / 构建输出最大字符数。

例如，希望明确固定路径并开启预热时，可在 config 中补充：

workspaceRoot: 'D:/lean4-harness-plugin/lean'
mathlibRoot: 'D:/mathlib4'
lakeCommand: 'lake'
leanCommand: 'lean'
prewarm: true
prewarmTimeoutMs: 90000

修改 cordis.patch.yml 或 package.json 后，需要重新安装 Bundle：

Set-Location D:\deepseek-harness\deepseek-harness
$env:DSH_HOME = 'D:\lean4-harness-plugin\.dsh-lean4-plugin-test'
pnpm dsh plugin --profile web remove lean4-harness-plugin
pnpm dsh plugin --profile web add 'link:D:\lean4-harness-plugin'
pnpm dsh --profile web --dump-config

lean4-harness-plugin

AI 分析

安装

说明文档

怎样使用

Harness 如何加载和使用插件

Bundle 配置