PSA: Lean MCP tools breakage with FastMCP

Stream: Machine Learning for Theorem Proving

[Gavin Zhao]

A few hours ago, the mcp Python package made a breaking change in a patch release, which breaks most if not all MCP tools. For us, this means all of the MCP tools in the Lean ecosystem are broken if you run them through uvx and are not pinning the dependencies, which is the default and recommended way to run them.

A temporary fix for this is to have mcp==1.12.2 in a requirements.txt file and add --with-requirements=requirements.txt as the first arugment to uvx. Alternatively, you can also set the environment variable UV_CONSTRAINT to the path of the requirements.txtfile, e.g.

{
  "mcpServers": {
    "lean-lsp": {
      "type": "stdio",
      "command": "uvx",
      "args": [
        "lean-lsp-mcp"
      ],
      "env": {
        "UV_CONSTRAINT": "requirements.txt"
      }
    }
  }
}

Edit: corrected typo from mcp==1.21.2 to mcp==1.12.2

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Small correction: mcp==1.12.2.

[Oliver Dressler]

Fix for lean-lsp-mcp is deployed. uvx was automatically updating dependencies. To prevent this in the future the dependencies were pinned (mcp[cli]==1.12.3 instead of mcp[cli]>=1.12.3).

Just restart the server to get the fix.