isabelle-pide-mcp

# Isabelle PIDE MCP 服务器 本仓库包含： 1. 一个模型上下文协议（MCP）服务器，为 AI 代理提供工具，以便与 Isabelle 理论和 ML 文件进行交互式工作，适用于 Isabelle/PIDE 会话。 MCP 是无头且与编辑器无关的。你可以让代理独立工作，也可以与 Isabelle/jEdit 或 Isabelle/VSCode 一起运行。 2. 一套关于如何有效使用 MCP 的代理技能，以及形式化任务和 Isabelle 的一般指导。 ## 使用说明 要开始使用（参见下面的详细信息），请安装 MCP，将其注册到编码代理，然后你可以开始提示。 要交互式地探索代理的更改，你也可以在旁边运行 Isabelle/jEdit 或 Isabelle/VSCode 会话，该会话使用 MCP（参见屏幕截图）。 <img width="2048" height="1242" alt="Isabelle/jEdit 和编码代理并排" src="./docs/jedit_and_coding_agent.png" /> **使用 MCP 时请注意以下事项：** - MCP 管理其自己的 PIDE 会话。特别是，这意味着编辑器的会话和 MCP 的会话是相互独立的。 例如，命令将由 MCP 会话和编辑器会话处理， 传递给编辑器会话的 Isabelle 选项（例如包含的会话目录）也必须传递给 MCP。 - 如果你编辑 MCP 正在使用的相同文件，则只有在更改写入磁盘后，MCP 才能看到这些更改。 MCP 会在每次读取和写入时自动与磁盘同步。 反之，如果通过 MCP 编辑文件，则可能需要在编辑器中手动重新加载文件，以防编辑器不自动重新加载磁盘上的更改。 在 Isabelle/jEdit 中，有时需要手动重新加载（例如，使用 F5 键）。Isabelle/VSCode 支持自动重新加载。 - 如果你希望代理在预构建的基础会话中看到证明状态，你必须使用 `-o show_states` 构建它们。 ## 安装 MCP 服务器 1. 安装支持的 Isabelle 版本。支持的版本存储在 [ISABELLE\_VERSION](./ISABELLE_VERSION) 中。较新版本也可能适用（但不保证）。将版本号插入以下命令中： ```bash hg clone https://isabelle.in.tum.de/repos/isabelle isabelle/Admin/init -r <版本号> ``` 2. 安装组件。将此目录的路径插入以下命令中： ```bash isabelle/bin/isabelle components -u <此目录的路径> ``` ## 运行 MCP 服务器 你可以将服务器注册到你的 MCP 客户端（例如 OpenCode、Claude Code、Codex 等），也可以手动启动服务器： ```bash isabelle/bin/isabelle pide_mcp -l HOL ``` 与往常一样，所有选项都可以使用 `pide_mcp -?` 显示（它们遵循典型的 Isabelle 约定，例如 `-d`、`-v`、`-L`）。 ### 连接编码代理到 MCP 服务器 - 对于 **OpenCode**，复制/调整 `.opencode` 文件夹，并在同一基准目录中启动 OpenCode。 - **你必须在 `.opencode/opencode.json` 中调整 Isabelle 的路径**，以及可能需要传递给 MCP 的选项（例如包含的会话目录）。 - 对于 **Claude Code**，复制/调整 `.claude` 和 `.mcp.json`，并在同一基准目录中启动 Claude Code。 - **你必须在 `.mcp.json` 中调整 Isabelle 的路径**，以及可能需要传递给 MCP 的选项（例如包含的会话目录）。 ## 代理技能 `skills` 文件夹（在 `.opencode/` 和 `.claude/` 中）包含以下 AI 代理的指导： - `isabelle-formalization`：形式化的指导原则和最佳实践。 - `isabelle-proof-development`：关于证明搜索、自动化和概念搜索的指导。 - `pide-mcp`：关于有效使用此 MCP 的指导。 你可以根据需要调整这些指导。 ## 已知限制/未来工作 - Isabelle2025-2 不受支持。第一个稳定版本计划用于 Isabelle2026。 - 预构建会话的命令计时目前返回为 0。 - 期望有一个选项可以共享 MCP 和编辑器（Isabelle/jEdit、Isabelle/VSCode）之间的 PIDE 会话。 这需要对 Isabelle 分发源进行更改。 - 期望在不更改受影响文档状态的情况下，使用 PIDE 探索更改， 参见 [Hanno Becker 的此电子邮件](https://isabelle.zulipchat.com/#narrow/channel/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Isabelle.2FREPL/near/581059372)。 这需要对 Isabelle 分发源进行更改。 - 支持动态扩展（“插件”），以便用户可以模块化地添加新的 MCP 工具。 ## 相关工作 [I/Q](https://github.com/awslabs/AutoCorrode/tree/main/iq) 是一个替代的 Isabelle MCP，它提供了一个以 Isabelle/jEdit 为中心的 workflow（使用共享文档状态）。 使用这两个系统的经验报告非常受欢迎：我们希望在未来能够结合两个 MCP 的优势。 ## 反馈、问题、讨论 请使用 [此 Isabelle Zulip 流](https://isabelle.zulipchat.com/#narrow/channel/202967-New-Members-.26-Projects/topic/PIDE.20MCP)。 或者，通过电子邮件联系 Kevin Kappelmann。