关键词

Lean定理证明LSPLanguage Server ProtocolAgentic交互

Lean LSP MCP服务器使用说明

项目简介

Lean LSP MCP 服务器是一个基于 Model Context Protocol (MCP) 构建的后端应用，它充当 LLM 客户端与 Lean 4 定理证明器之间的桥梁。通过此服务器，LLM 客户端可以利用预定义的工具集，与 Lean 4 LSP（Language Server Protocol）服务器进行交互，从而实现对 Lean 项目的 Agentic 控制，例如自动定理证明、代码诊断、目标查询等。

主要功能点

  • 提供与 Lean 4 定理证明器交互的工具集: 服务器内置了一系列工具，允许 LLM 客户端查询 Lean 项目信息、文件内容、诊断信息、证明目标，以及执行重启 LSP 服务器等操作。
  • 支持 Agentic 定理证明: 通过集成 Lean LSP 客户端，服务器能够响应 LLM 客户端的请求，执行 Lean 定理证明相关的操作，辅助 LLM 完成自动定理证明任务。
  • 基于 MCP 协议: 遵循 Model Context Protocol 标准，确保与支持 MCP 协议的 LLM 客户端（如 VS Code Agent Mode, Cursor, Claude Desktop, OpenAI Agent SDK 等）的兼容性和互操作性。
  • 灵活配置: 允许用户通过环境变量 'LEAN_PROJECT_PATH' 指定 Lean 项目的根目录，以适应不同的项目环境。

安装步骤

  1. 安装 uv: uv 是一个 Python 包管理器，用于安装和管理 Python 依赖。请根据 uv 官方文档 安装适合您系统的 uv。例如，在 Linux/MacOS 上，可以运行命令： 
    curl -LsSf https://astral.sh/uv/install.sh | sh
  2. 安装 lean-lsp-mcp: 使用 uv 安装 'lean-lsp-mcp' 包。 
    uv pip install lean-lsp-mcp
  3. 配置环境变量 'LEAN_PROJECT_PATH': 设置环境变量 'LEAN_PROJECT_PATH' 指向您的 Lean 项目根目录。这是服务器正常运行的必要条件。例如，如果您在 Linux/MacOS 上使用 bash，可以将以下行添加到您的 '~/.bashrc' 或 '~/.zshrc' 文件中，并将 '/path/to/lean/project' 替换为您的实际 Lean 项目路径： 
    export LEAN_PROJECT_PATH="/path/to/lean/project"
    然后运行 'source ~/.bashrc' 或 'source ~/.zshrc' 使环境变量生效。

服务器配置

MCP 服务器需要配置在 MCP 客户端中才能使用。以下是针对不同 MCP 客户端的服务器配置示例。您需要将这些配置信息添加到您的 MCP 客户端设置中。

针对 VS Code Insiders (Agent Mode) 的配置 (settings.json):

{
    "mcp": {
        "servers": {
            "lean-lsp": {  // 服务器名称，客户端使用此名称引用该服务器
                "command": ["uvx"], // 启动服务器的命令，这里使用 uvx 启动
                "args": ["lean-lsp-mcp"], // 启动服务器的参数，这里指定运行 lean-lsp-mcp
                "env": {
                    "LEAN_PROJECT_PATH": "/path/to/lean/project" // Lean 项目根目录，**请替换为您的实际项目路径**
                }
            }
        }
    }
}

针对 Cursor 的配置 (mcp.json):

{
    "mcpServers": {
        "lean-lsp": {  // 服务器名称，客户端使用此名称引用该服务器
            "command": "uvx", // 启动服务器的命令，这里使用 uvx 启动
            "args": ["lean-lsp-mcp"], // 启动服务器的参数，这里指定运行 lean-lsp-mcp
            "env": {
                "LEAN_PROJECT_PATH": "/path/to/lean/project" // Lean 项目根目录，**请替换为您的实际项目路径**
            }
        }
    }
}

配置说明:

  • '"servers"' 或 '"mcpServers"': 定义 MCP 服务器配置的顶级键。
  • '"lean-lsp"': 服务器名称，您可以自定义，客户端通过此名称引用该服务器。
  • '"command"': 启动服务器的可执行命令。 'uvx' 是 'uv run' 的快捷方式，用于在 uv 环境中运行 Python 脚本或模块。
  • '"args"': 传递给启动命令的参数。 '"lean-lsp-mcp"' 指定要运行的 Python 模块是 'lean-lsp-mcp'。
  • '"env"': 传递给服务器进程的环境变量。 'LEAN_PROJECT_PATH' 必须设置为您的 Lean 项目根目录。 请务必将 '/path/to/lean/project' 替换为您的实际 Lean 项目路径。

基本使用方法

  1. 确保已正确安装 uv, lean-lsp-mcp，并配置了 'LEAN_PROJECT_PATH' 环境变量。
  2. 在 MCP 客户端（如 VS Code Insiders 或 Cursor）中，根据上述配置示例添加并启用 'lean-lsp' 服务器。
  3. 打开一个 Lean ('.lean') 文件。
  4. 在 MCP 客户端的 Agent 模式下，您可以使用预定义的工具与 Lean LSP MCP 服务器进行交互，例如：
    • 使用 'lean_goal' 工具查询当前证明目标。
    • 使用 'lean_diagnostic_messages' 工具获取代码诊断信息。
    • 使用 'lean_auto_proof_instructions' 工具获取自动证明的指导。
    • 等等。
  5. 具体工具的使用方法请参考工具的描述信息。

注意事项

  • 首次使用或 Lean 项目发生重大更改后，可能需要重启 LSP 服务器 ('lean_lsp_restart' 工具) 或重建 Lean 项目以确保功能正常。
  • 部分工具（如 'lean_lsp_restart'）执行时间较长，请耐心等待。
  • 详细的工具列表和使用说明请参考仓库的 README 文档。

信息

分类

开发者工具

访问项目