Metadata-Version: 2.4
Name: isabelle-mcp
Version: 0.6.0
Summary: MCP server bridging AI agents with the Isabelle proof assistant via its LSP/PIDE interface
Author-email: Qiyuan Xu <xqyww123@gmail.com>
License-Expression: LGPL-2.1-or-later
Project-URL: Homepage, https://github.com/xqyww123/Isabelle-MCP
Project-URL: Documentation, https://github.com/xqyww123/Isabelle-MCP/tree/main/docs
Project-URL: Repository, https://github.com/xqyww123/Isabelle-MCP
Project-URL: Issues, https://github.com/xqyww123/Isabelle-MCP/issues
Project-URL: Changelog, https://github.com/xqyww123/Isabelle-MCP/blob/main/CHANGELOG.md
Keywords: isabelle,theorem-prover,mcp,lsp,ai-assistance
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Libraries :: Python Modules
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Typing :: Typed
Requires-Python: >=3.12
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: anyio>=4.0.0
Requires-Dist: beautifulsoup4>=4.12.0
Requires-Dist: fastmcp<4,>=3.2
Requires-Dist: mcp>=1.0.0
Requires-Dist: pydantic>=2.0.0
Requires-Dist: pyyaml>=6.0
Requires-Dist: watchdog>=3.0.0
Provides-Extra: dev
Requires-Dist: coverage>=7.0.0; extra == "dev"
Requires-Dist: pytest>=7.0.0; extra == "dev"
Requires-Dist: pytest-asyncio>=0.21.0; extra == "dev"
Requires-Dist: pytest-cov>=7.0.0; extra == "dev"
Requires-Dist: mypy>=1.0.0; extra == "dev"
Requires-Dist: black>=23.0.0; extra == "dev"
Requires-Dist: ruff>=0.1.0; extra == "dev"
Dynamic: license-file

# Isabelle-MCP

[![PyPI](https://img.shields.io/pypi/v/isabelle-mcp)](https://pypi.org/project/isabelle-mcp/)
[![Python](https://img.shields.io/badge/python-%E2%89%A5%203.12-blue)](https://pypi.org/project/isabelle-mcp/)
[![CI](https://github.com/xqyww123/Isabelle-MCP/actions/workflows/ci.yml/badge.svg)](https://github.com/xqyww123/Isabelle-MCP/actions/workflows/ci.yml)
[![License: LGPL-2.1-or-later](https://img.shields.io/badge/license-LGPL--2.1--or--later-blue)](LICENSE)

MCP server that lets AI agents (Claude Code, Codex, …) drive the Isabelle
theorem prover through its LSP/PIDE commands — fully autonomously, with no
human in the loop.

## Purpose

This MCP server exists so that Claude / Codex can issue Isabelle LSP commands
**without any human mediation**. The entire Isabelle process is encapsulated
behind the MCP tools — it exposes **no UI to the user**. The agent works by
editing `.thy`/`.ML` files on disk and calling the tools to evaluate them and
query proof states; nobody watches or steers the prover interactively.

This server is **not designed for human–AI collaboration** (there is no
jEdit/VSCode front-end in the picture). It implements a single
AI ↔ Isabelle, no-human-in-the-loop model.

> ⚠️ **One agent per server instance.** This server holds a single Isabelle
> session with global mutable state — one set of open documents, one
> perspective, and one evaluation in flight at a time. It is
> **single-threaded and not concurrency-safe**: pointing multiple agents at one
> instance, or interleaving concurrent requests, corrupts the evaluation and
> document state with catastrophic, hard-to-debug results. The server runs over
> **stdio**, so each agent already gets its own dedicated server process (and its
> own `isabelle mcp_server`) — just don't share one or drive it concurrently.

> [!IMPORTANT]
> **No Isabelle patch is needed.** Earlier versions required one: the server drove the
> stock `isabelle vscode_server`, which lacks the PIDE requests it needs, so the
> distribution had to be patched. It no longer does. Isabelle-MCP now ships its own
> Isabelle Scala component — `isabelle mcp_server` — and registers it with your Isabelle
> the first time you launch a session. Nothing is compiled on your machine (the component
> carries a prebuilt jar and declares `no_build = true`), so `site-packages` may even be
> read-only, and **no session heap is invalidated**.
>
> Requirements: **Isabelle2025-2**, with `isabelle` on `PATH` (or pinned with
> `isabelle-mcp install --isabelle-bin /path/to/Isabelle/bin/isabelle`). Isabelle2024 is
> no longer supported — see the `last-isabelle2024-support` tag.
>
> To undo the registration: `isabelle-mcp uninstall`. If you remove the package without
> it, Isabelle will print `### Missing Isabelle component: …` on every command until you
> run `isabelle components -x <the path it names>` — harmless, but noisy.

## Quick Start

```bash
pip install isabelle-mcp      # or: uv tool install isabelle-mcp

# register into Claude Code / Codex (auto-detects whichever is installed):
isabelle-mcp install
```

For Claude Desktop, register manually instead
(`~/.config/claude/claude_desktop_config.json`):

```json
{
  "mcpServers": {
    "isabelle": {
      "command": "isabelle-mcp"
    }
  }
}
```

## Tools

| Tool | Description |
|------|-------------|
| `isabelle_launch` | Start (or restart) the prover with the session/logic that fits the work (bare `Main` is only a minimal fallback); **call this first** |
| `isabelle_terminate` | Terminate the running prover (the MCP server stays up; you can relaunch) |
| `isabelle_evaluate_to` | Evaluate the theory up to a line; returns a per-file snapshot of errors / sorry / running command lines |
| `isabelle_evaluation_status` | Poll progress of a running evaluation (same snapshot) |
| `isabelle_cancel_evaluation` | Cancel a running evaluation |
| `isabelle_hover` | Type info and documentation at position |
| `isabelle_definition` | Jump to symbol definition |
| `isabelle_local_occurrences` | In-file occurrences (definition + uses) of a local entity |
| `isabelle_goal` | **Proof goals** — omit after_text for before/after diff |
| `isabelle_find_theorems` | Search the theorem database in the context at a position (Isabelle's `find_theorems`): by name, pattern, intro/elim/dest, solves, simp |
| `isabelle_command_output` | Prover output messages |
| `isabelle_command_status` | What state the command(s) covering each of several lines are in |
| `isabelle_session_info` | Current session info |

With `isabelle_launch(session, debug=true)` the **ML debugger** tools come alive
(eleven more tools): set/delete/list breakpoints on compiled Isabelle/ML code
(`isabelle_set_breakpoint`, `isabelle_del_breakpoints`,
`isabelle_list_breakpoints`, `isabelle_list_breakable_sites`), arm and disarm
them in bulk (`isabelle_enable_all_breakpoints`,
`isabelle_disable_all_breakpoints`), and work with **hits** — threads stopped
at a breakpoint: inspect (`isabelle_debug_state`), evaluate ML in a stack
frame's scope (`isabelle_eval_at_breakpoint`), print a frame's locals
(`isabelle_locals_at_breakpoint`), resume (`isabelle_continue_breakpoint`) and
single-step (`isabelle_step_at_breakpoint`). A hit pauses the evaluation: the
`isabelle_evaluate_to` result leads with a hit report (position, call stack,
frame-0 locals), and asynchronous events arrive as one-line *debugger notices*
on the next tool result. The full design lives in
[`docs/archive/DEBUGGER_DESIGN.md`](docs/archive/DEBUGGER_DESIGN.md).

All positions are **1-indexed**. File paths must be **absolute**.

Every query tool names a file and a line, and the prover answers about the
command there without moving its caret — so a query can run while an evaluation
is in progress, and it may only be refused for the position it asked about, not
because the session is busy. A query that cannot produce a result says why
("this command is not a proof operation", "it has not finished evaluating");
nothing is concluded from a timeout.

## Development

```bash
pip install -e ".[dev]"             # editable install from a checkout
pytest                              # unit tests
pytest -m integration               # requires running Isabelle
python -m mypy src/                 # type checking
```

## Architecture

```
server.py         FastMCP entry point — tool registration, lifespan
lsp_client.py     JSON-RPC 2.0 client for isabelle mcp_server
tools/            Tool implementations (one file per tool)
utils/            Position conversion, URI handling, HTML parsing
models.py         Pydantic output models
```

## License

Copyright © 2024-2026 Qiyuan Xu.

This project is free software: you can redistribute it and/or modify it under
the terms of the GNU Lesser General Public License as published by the Free
Software Foundation, either version 2.1 of the License, or (at your option) any
later version. See [LICENSE](LICENSE) for the full text.
