Skip to content

Installer: add native Pi (pi.dev) MCP registration #286

@jonathan-nicoletti

Description

@jonathan-nicoletti

Summary

The ProofKit installer auto-registers proofkit-mcp with Claude Desktop, Claude Code, Cursor, Codex, VS Code, Windsurf, and Gemini CLI. It does not support Pi, so Pi users currently have to configure ProofKit by hand.

PR #285 documents the manual Pi path. This issue tracks making it automatic, like the other agents.

Background: why Pi is a bit different

Unlike the currently-supported agents, Pi has no built-in MCP support. It cannot launch proofkit-mcp on its own — a community MCP-bridge extension must be installed first (e.g. pi-mcp-adapter). Once that adapter is present, Pi reads a standard mcpServers config, so the existing server entry shape works unchanged.

Proposed installer behavior

  1. Detect Pi. Presence of the Pi agent dir ~/.pi/agent/ (or $PI_CODING_AGENT_DIR) is a reliable signal.

  2. Write the server entry to ~/.pi/agent/mcp.json under the standard mcpServers key — identical shape to the Claude Desktop/Cursor entries the installer already writes:

    {
      "mcpServers": {
        "proofkit-mcp": {
          "command": "/Users/you/.local/bin/proofkit-mcp",
          "args": [],
          "env": {}
        }
      }
    }
  3. Optionally note the adapter dependency. Since Pi needs an MCP bridge extension, the installer could either:

    • just write the config and surface a one-line message ("Pi detected — run pi install npm:pi-mcp-adapter, then restart Pi"), or
    • leave adapter installation to the user and rely on the docs.

    Writing only the standard config file (and not depending on any specific adapter) keeps users free to use any MCP bridge.

Notes / open questions

  • ~/.pi/agent/mcp.json is the Pi-global override path read by pi-mcp-adapter; pi-mcp-extension is another option. Writing the vendor-neutral mcpServers file is the safest target.
  • Adapter-specific niceties like lifecycle: "eager" and directTools: true are optional and probably shouldn't be written by the installer by default (they're adapter-specific, not part of the core entry).
  • The agent-registration logic lives in the native installer (not this repo), so this is an installer-side change.

Verification already done

Manually wired this up locally: installed pi-mcp-adapter, added the proofkit-mcp entry to ~/.pi/agent/mcp.json, restarted Pi, and confirmed connectedFiles + layout_metadata worked and the 16 ProofKit tools registered as first-class Pi tools.

Related

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions