PIDE MCP · New Members & Projects

From your perspective, are there already any philosophical or design differences between your Isabelle MCP and I/Q?

Kevin Kappelmann (Jun 30 2026 at 14:55):

One difference is that I/Q connects to jEdit whereas PIDE MCP works through a headless PIDE session.

The set of tools offered by I/Q (listed here) and PIDE MCP (listed here) are different.

Both are fairly easy to set up, so you could simply experiment with both and see which one fits your framework better :)

András Salamon (Jul 02 2026 at 16:36):

I see that this requires Isabelle version c13a4bd3c018 i.e. 20 May 2026, so no support for 2025-2. What was the big change in Isabelle between these two changesets that requires the more recent one for the PIDE access?

Kevin Kappelmann (Jul 03 2026 at 07:04):

Just some changes in the Isabelle/Scala signatures. When you compile PIDE MCP with Isabelle2025-2, you can see the compile errors. An Isabelle2025-2 compatible branch would be very welcomed as a contribution if you want to give it a go.

Yutaka Nagashima (Jul 06 2026 at 00:03):

Do you already have a preferred way for people to cite this project? :slight_smile:

Kevin Kappelmann (Jul 06 2026 at 10:58):

Yong Kiam (Jul 10 2026 at 16:13):

thanks for this work. I'm trying this out and it seems to work, but I've ran into an issue multiple times (which I can't diagnose) where the interface just seems to hang with no progress. The only way to recover is for me to manually restart the mcp (which works but certainly isn't ideal).

Yong Kiam (Jul 10 2026 at 16:48):

if there's a better report or information that you need, let me know and I can try to get that the next time I hit a freeze

Kevin Kappelmann (Jul 13 2026 at 08:35):

Let me address the agent's comments one by one (at least the ones I understand):

The agent mixed two different ways to refer to a theory: absolute file paths vs. session-qualified. Your shared text indicates that it edited the theory of a base session using an absolute file path but then requested (and imported) that theory session-qualified. But session-qualified base session theories are read-only and changes will not propagate. To see the changes, it also needs to use an absolute import. To try this yourself, start Isabelle with base session HOL and then compare importing and editing "~~/src/HOL/HOL" vs "HOL.HOL". Only if you import using the former you will see any changes propagate. The import of the latter is instant, the former will process the dependencies.

I don't know your intended application, but there is a good chance that you do not want the agent to use absolute file paths for base sessions because doing so will re-process the required theories (which is very slow). To this end, there is even a hint for the agent in the PIDE MCP SKILL file.

Finally, this mismatch/mixed usage of absolute file paths and session-qualified references might also have caused what it calls "Symptom 2", essentially a situation where it believes (rightfully or not) to be stuck. Another possible cause is that there are non-terminating commands in some theory file that it did not consider which block the processing of the commands that it is waiting for. The model is then confused as to why the commands it is waiting for are never processed/updated. I have a suspicion that this occurred to me and my collaborators a number of times before. A possible remedy might be to write an MCP tool that provides the agent an overview of all loaded theories and their progress (akin to the progress bar in Isabelle/jEdit). This way, it could locate where Isabelle is stuck (or if the process really stopped responding). Maybe this is likely caus in your case too?

You can enable writing a log file by passing the -L <file_name> option to PIDE MCP (see isabelle pide_mcp -? for all options). Note, however, that the log file logs all requests and responses, so don't share it blindly if you are doing "secret" work.

Yong Kiam (Jul 13 2026 at 08:46):

thanks! I'll check this out the next time I get around to it (which might be after FLOC)

Kevin Kappelmann (Jul 13 2026 at 08:49):

I'm also at the Isabelle Workshop and ITP - hit me up if you wanna try out some things :)

Yong Kiam (Jul 13 2026 at 08:50):

Balazs Toth (Jul 13 2026 at 14:08):

I’ve been experimenting with coding-agent hooks for Isabelle proof discipline:

The hooks currently discourage apply scripts and require search-discoverable terminal proof methods to have recent sledgehammer/try0 evidence. They inspect newly added theory text and support Claude Code, Codex, and OpenCode, including AutoCorrode I/Q and isabelle-pide-mcp.

I’ve manually tested the setup with all three agents. It is deliberately best-effort and fail-open, since agent hook and transcript interfaces are still evolving. Feedback would be very welcome.

Kevin Kappelmann (Jul 25 2026 at 11:11):

We have a short workshop to set up an AI with Isabelle at 13:15 in the Isabelle workshop room at FLoC if anybody wants to join.

Kevin Kappelmann (Jul 26 2026 at 14:18):

The new tools are also available on the Isabelle2025-2 compatible branch 2025-2. We hope the tools improve the efficiency of the MCP particularly in large session applications. Feedback is very welcomed.

Junming Zhao (Jul 27 2026 at 10:41):

To update the MCP server, do I sync the mcp repository and re-run the isabelle/bin/isabelle components -u .. installation line?

Kevin Kappelmann (Jul 27 2026 at 12:05):

You just need to pull from the repository. Isabelle will detect that the component changed and rebuild it automatically

Junming Zhao (Jul 27 2026 at 12:40):

Kevin Kappelmann (Jul 27 2026 at 14:22):

One note: I unfortunately named the 2025-2 release tag the same as the 2025-2 branch. So make sure you are pulling the newest changes from the branch and you're not on the tag.

Kevin Kappelmann (Jul 27 2026 at 15:56):

Yong Kiam (Jul 30 2026 at 01:45):

I think somewhere in the README there could be an "official" recommendation for setting up
prebuilt heaps (and also what to do if the heap changes mid-project)

it looks like the -l HOL gets baked into the MCP JSON at setup (at least with Claude Code)

Qiyuan Xu (Jul 30 2026 at 02:20):

My experience is that claude/codex can parse the ROOT structure and pick up the right base session it needs, if sufficient instruction/prompt is provided

Kevin Kappelmann (Jul 30 2026 at 13:30):

I'll add a note to the README.
Changing the base session on the fly is currently not supported. To change the base session, one has to change the -l option (in the mcp json) and then restart the MCP. I think(?) most coding agents do not allow agents to restart MCPs on their own though.

Qiyuan Xu (Jul 30 2026 at 14:58):

Right, coding agents generally won't restart an MCP server on their own. What I do is decouple the Isabelle session/process from the MCP itself. Each time an agent (Claude/Codex) starts up, only a thin Python wrapper is launched automatically — the actual Isabelle process isn't spawned until Claude/Codex makes its first call to the MCP. This lazy initialization avoids launching a full Isabelle instance every time I start Claude/Codex, which matters when that session isn't going to touch Isabelle at all (especially since I usually have ~10 Claude instances running in parallel; otherwise I'd end up with 10 Isabelle instances on my laptop :-)

Diego Marmsoler (Aug 13 2026 at 09:02):

I am playing around with the PIDE MCP server currently and it works quite well. Thanks.

I do have a question, though. I observed that an MCP get_state call made immediately after a successful edit response can still use the document version from before the edit.

I am not sure whether this is intended asynchronous behavior or whether a successful edit is expected to establish that a subsequent sequential get_state sees the edited document.

I produced a small reproduction against the original Isabelle2025-2 server implementation. The client:

After a short retry, line 12 is available. The inverse operation shows the same behavior: after shrinking the theory back to 11 lines and receiving the successful edit response, an immediate get_state still accepts line 12 from the previous version.

This is not caused by pipelined or concurrent client requests: the reproduction waits for each edit response before sending get_state.

I repeated the expand-and-shrink experiment several times. In every case, the first get_state after the successful edit response still observed the previous document version; a short retry then observed the new version.

My reading of the implementation is that Session.update returns after the update has been accepted by the session manager, while Document.State.snapshot uses the most recent stable document version. The new version may therefore not yet be the stable tip when get_state runs.

So in summary, i think that currently the behaviour is as follows:
A successful edit only queues/submits the PIDE update, and callers are expected to retry get_state; or

An alternative behaviour would be the following:
A successful edit guarantees that a subsequent sequential get_state uses the document version containing that edit, although command evaluation may still be running.

session.update(...)
session.await_stable_snapshot()

With that wait after theory text edits, the same reproduction produced no stale observations. I also tested it with a larger payload to widen the previous timing window.

The change only waits for the edited document version to become the stable history tip; it does not wait for all proof commands to finish evaluating.

If this is actually the intended behaviour, I would be happy to open a GitHub pull request containing the minimal fix and the reproduction/regression test.

Diego Marmsoler (Aug 13 2026 at 12:18):

On a related note, I also investigated concurrent calls to the PIDE MCP edit tool and wanted to check whether concurrent edits to the same document are expected to be supported.

It seems that the server dispatches tool calls concurrently. Each edit independently reads the current document, computes a complete updated file, writes it to disk, and submits incremental edits to PIDE.

Using a small theory containing two distinct markers, I submitted two concurrent edits:

disk: LEFT_NEW ... RIGHT_OLD
PIDE: LEFT_NEW ... RIGHT_NEW

Thus, one complete-file disk write overwrote the other, while PIDE applied both incremental edits. This reproduced repeatedly, including without artificial padding. Concurrent edits to different theories remained consistent.

Concurrent replacements at the same location were timing-dependent. Sometimes the second request was rejected correctly, but I also observed both requests succeeding, disk and PIDE selecting different results, and once Isabelle’s change_parser reporting requirement failed: bad text edit.

The same race occurred when one request used a relative theory path and the other used its absolute path. Therefore, any synchronization would presumably need to use the resolved document identity rather than the raw request string.

Even if concurrent edits to the same document are considered unsupported caller behavior, should the server serialize them or reject one explicitly? Returning two successful responses while leaving disk and PIDE inconsistent was unexpected for me.

Again, I have fixed this locally using per-session, per-canonical-document synchronization and added a regression test. If you think this approach fits the intended API semantics, I would be happy to submit a pull request for this too.

Kevin Kappelmann (Aug 13 2026 at 14:57):

I have an upcoming change for the edit tool that might fix some of these issues. Who is Diego and how would I get in contact with him?

Kevin Kappelmann (Aug 13 2026 at 22:38):

Sorry, I thought the messages were sent by someone else and not you directly @Diego Marmsoler :sweat_smile: will look into it when I'm back to work next week

Kevin Kappelmann (Aug 18 2026 at 17:14):

Yes, get_state takes the latest stable snapshot, which might not contain the latest edits yet. I deliberately didn't use await_stable_snapshot because it may block (possibly even indefinitely on rapid edits). Having just introduced synchronised edits, I reconsidered this decision and now use await_stable_snapshot in editing-operations.
These changes are also available in the Isabelle2025-2 branch.

Kevin Kappelmann (Aug 18 2026 at 17:17):

They weren't "supported" (i.e. conflicts as reported by you were expected), but I now introduced synchronised edits, which should rule out such behaviours in the future.
These changes are also available in the Isabelle2025-2 branch.

Kevin Kappelmann (Aug 18 2026 at 17:18):

This and similar stuck process issues should also be resolved now (both on main and Isabelle2025-2).

Kevin Kappelmann (Aug 21 2026 at 17:06):

Unfortunately, I introduced a performance regression in the latest changes that significantly slows down applications using a large number of dynamic dependencies.

I'm working on a patch. If you are affected, please use an older commit in the meantime. (thanks to @Diego Marmsoler for reporting it)

Kevin Kappelmann (Aug 24 2026 at 15:06):

This should be resolved now on main and Isabelle2025-2, along with several other improvements (cf. NEWS).

Mohammad Abdulaziz (Aug 25 2026 at 12:36):

Kevin Kappelmann (Aug 25 2026 at 12:37):

Kevin Kappelmann (Aug 25 2026 at 12:41):

Note that the code might not work with the newest PIDE MCP version due to several API changes I did in the last couple of days.
It probably works with commit 002a26bad93593d6b1f90fa2c90e1291a302d1ad of PIDE MCP.
Alternatively, tell your agent to make it compatible again and hope for the best ;)

Yong Kiam (Aug 26 2026 at 02:48):

Kevin Kappelmann (Aug 26 2026 at 07:38):

Oops, indeed - Mohammad accidentally posted it on the wrong channel (I moved it to the right one now) and I replied without noticing. For clarification, we have some group work as part of below project:

Stream: New Members & Projects

Topic: PIDE MCP

Kevin Kappelmann (Jun 30 2026 at 07:07):

Yutaka Nagashima (Jun 30 2026 at 13:55):