lean4-mcp代理
一个MCP（模型上下文协议）服务器，在AI代理和精益4语言服务器之间代理。它允许代理打开精益文件，检查错误，检查证明目标，并通过标准MCP工具调用界面编辑文档。
：警告： 平台支持：在Linux上测试。不保证支持Windows和macOS。
特性
- 打开文件 从磁盘或内存中，自动检测Lake工作区
- 获取诊断信息 精益完成类型检查后（错误、警告）
- 查询证明目标 在战术块内的任何光标位置
- 编辑文档 --完全替换或目标范围编辑
工具
| 工具 | 说明 |
|---|---|
open_file | 打开a .lean 按路径从磁盘中提取文件（自动检测Lake工作区） |
open_document | 按URI+文本内容打开文件 |
get_diagnostics | 获取编译错误/警告（等待精益完成） |
get_goal_state | 查询某个位置的策略证明状态 |
replace_document | 替换整个文件内容 |
apply_edit | 应用目标范围编辑 |
get_document_text | 读取当前文档内容 |
close_document | 关闭文档并释放资源 |
file_status | 检查Lean是否仍在处理文件 |
list_documents | 列出所有工作区中的所有打开文档 |
先决条件
构建
cargo build --release二进制文件位于 target/release/lean4-mcp-proxy.
用法
VS代码/光标设置
步骤1：构建MCP服务器
cargo build --release二进制文件将位于 target/release/lean4-mcp-proxy.
步骤2：配置MCP设置
对于带有Cline/Roo-Cline的VS代码：
- 打开VS代码设置（Cmd/Ctrl+，）
- 搜索“MCP”或导航到您的MCP扩展设置
- 将服务器配置添加到MCP设置文件中（通常
.vscode/mcp.json或全局设置）：
{
"mcpServers": {
"lean4-mcp": {
"command": "/absolute/path/to/lean4-mcp-proxy",
"args": []
}
}
}对于光标：
- 打开光标设置→ 特性→ 模型上下文协议
- 添加一个新的MCP服务器：
- 名字: lean4-mcp - 命令: /absolute/path/to/lean4-mcp-proxy - 参数：（留空以供自动检测）
步骤3：验证安装
重新启动编辑器后，MCP服务器应出现在MCP工具列表中。您可以通过以下方式进行验证：
- 打开精益4文件(
.lean) - 让你的人工智能助手“列出可用的MCP工具”
- 你应该看到这样的工具
open_file,get_diagnostics,get_goal_state等等。
步骤4：与Lake项目一起使用
湖工作区是从以下位置自动检测到的 lakefile.lean 当你打开一个文件时。对于默认项目，请使用：
{
"mcpServers": {
"lean4-mcp": {
"command": "/absolute/path/to/lean4-mcp-proxy",
"args": ["--lake-project", "/path/to/your/lake/project"]
}
}
}环境变量
| 变量 | 描述 |
|---|---|
LAKE_PROJECT | 默认Lake项目根（替代 --lake-project) |
LEAN_BIN | 自定义路径 lean 二进制 |
LAKE_BIN | 自定义路径 lake 二进制 |
RUST_LOG | 日志级别(info, debug, trace)--日志转到stderr |
协议
通过以下方式进行沟通 标准 使用换行符分隔的JSON-RPC（MCP协议版本 2024-11-05).代理将MCP工具调用转换为对精益4语言服务器的LSP请求。