lean-lsp-mcp

If a tool requires long-running state (e.g., a subprocess or cache) or needs rate limiting, you must modify server.py.

Adding Lifespan State

1. Add the field to the AppContext dataclass in server.py.
2. Initialize the resource in app_lifespan after lean_project_path is computed.
3. Ensure cleanup in the finally block of app_lifespan.

Rate Limiting

To protect remote services, use the @rate_limited decorator. You must first register the category in the rate_limit dictionary within app_lifespan.

# Example rate limit usage
@rate_limited("my_tool", max_requests=3, per_seconds=30)
@mcp.tool(...)
async def my_tool(ctx: Context, ...):
    ...

# In server.py
@dataclass
class AppContext:
    ... 
    my_thing: MyThing | None = None

# Inside app_lifespan
my_thing = await initialise_my_thing(lean_project_path)
context = AppContext(..., my_thing=my_thing)

# In the finally block
if context and context.my_thing:
    await context.my_thing.close()

To use lean-lsp-mcp with OpenAI surfaces (like ChatGPT) without exposing it to the public internet, use the OpenAI Secure MCP Tunnel.

1. Create a tunnel in OpenAI Platform settings.
2. Run tunnel-client on a host that can reach your Lean project.

For stdio transport:

export CONTROL_PLANE_API_KEY="sk-..."

tunnel-client init \
  --sample sample_mcp_stdio_local \
  --profile lean-lsp-local \
  --tunnel-id tunnel_0123456789abcdef0123456789abcdef \
  --mcp-command "uvx lean-lsp-mcp --transport stdio --lean-project-path /path/to/lean/project"

tunnel-client run --profile lean-lsp-local

For streamable-http transport: Bind the server to loopback and use the --mcp-server-url in your tunnel profile:

export LEAN_PROJECT_PATH="/path/to/lean/project"
uvx lean-lsp-mcp --transport streamable-http --host 127.0.1 --port 8000

You can configure the lean-lsp server in VSCode using the setup wizard or by manually editing your mcp.json configuration.

Using the Setup Wizard:

1. Press Ctrl+Shift+P.
2. Select MCP: Add Server....
3. Select Command (stdio).
4. Enter uvx lean-lsp-mcp as the command.
5. Name it lean-lsp.
6. Choose Global or Workspace.

Manual Configuration (User Settings): Open your user configuration via Ctrl+Shift+P > MCP: Open User Configuration and add:

{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "uvx",
            "args": [
                "lean-lsp-mcp"
            ]
        }
    }
}

WSL2 Users (Windows): If you are developing in WSL2, use this configuration instead:

{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "wsl.exe",
            "args": [
                "uvx",
                "lean-lsp-mcp"
            ]
        }
    }
}

To add a new tool to the lean-lsp-mcp server, follow this structured workflow to ensure proper integration with the MCP lifecycle and Lean LSP client:

1. Define the return model: Create a Pydantic model in src/lean_lsp_mcp/models.py. Use the wrapper pattern (a top-level model containing a list field) rather than returning a bare list. Use Optional[...] with a None default for optional fields.
2. Implement logic in a helper module: Place the heavy lifting (LSP calls, data processing) in a separate helper module (e.g., src/lean_lsp_mcp/utils.py). This module should be plain Python and should not import MCP-specific components, making it easier to test.
3. Register the tool in server.py: Use the @mcp.tool decorator to register the function.
   • The decorator argument is the public identifier string.
   • Use ToolAnnotations to provide metadata like title, readOnlyHint, idempotentHint, and openWorldHint.
   • The function signature must have ctx: Context as the first argument.
   • Use Annotated with Field for parameter descriptions and constraints.
   • The tool body should: validate the path using setup_client_for_file, retrieve the client from ctx.request_context.lifespan_context.client, and delegate to the helper module.
4. Handle Lifespan State: If the tool requires new state that persists across requests, initialize it inside app_lifespan after lean_project_path is computed, and ensure it is cleaned up in the finally block.

@mcp.tool(
    "tool_name",
    annotations=ToolAnnotations(
        title="Tool Title",
        readOnlyHint=True,
        idempotentHint=True,
        openWorldHint=False,
    ),
)\ndef tool_function(
    ctx: Context,
    param: Annotated[str, Field(description="Description")]
) -> ReturnModel:
    """One-line docstring."""
    # 1. Validate path
    # 2. Get client from ctx.request_context.lifespan_context.client
    # 3. Call helper
    return helper_function(client, param)