Kevin Kappelmann (Jun 30 2026 at 07:07): Kevin Kappelmann (Jun 30 2026 at 07:07):This is the discussion channel for PIDE MCP
Yutaka Nagashima (Jun 30 2026 at 13:55):@Kevin Kappelmann
Note that I/Q is an alternative Isabelle MCP which provides an Isabelle/jEdit-centred workflow.
Experience reports using both systems are very welcome: we hope that the strengths of both MCPs can be combined in the future.
I’d be interested in incorporating this into AbductionProver.
From your perspective, are there already any philosophical or design differences between your Isabelle MCP and I/Q?
I'm curious whether the two systems have different long-term goals.
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):Yutaka Nagashima said:
Do you already have a preferred way for people to cite this project? :slight_smile:
I now added citation information and a Zenodo release: https://github.com/kappelmann/isabelle-pide-mcp#citation
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).
FWIW, here's what Claude thinks:
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):Yong Kiam said:
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).
FWIW, here's what Claude thinks:
Let me address the agent's comments one by one (at least the ones I understand):
One earlier scratch was given a nonexistent import (
HOL-Library.Permutations).
After that, EVERY MCP operation on that scratch (read, correctiveedit)
failed with the import error, so it could not be repaired through the MCP
This has been fixed in the meantime.
Symptom 1: file-path node vs session-qualified node diverge
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):Kevin Kappelmann said:
I'm also at the Isabelle Workshop and ITP - hit me up if you wanna try out some things :)
sounds good, I'll look for you at the workshop.
Balazs Toth (Jul 13 2026 at 14:08):I’ve been experimenting with coding-agent hooks for Isabelle proof discipline:
https://github.com/balazstothofficial/isabelle-agent-hooks
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.
Disclaimer: The code was mostly written by Claude.
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):New in PIDE MCP:
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):thanks!
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):There's now an Isabelle2025-2 branch to fix this issue.
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 :-)
Last updated: Aug 05 2026 at 21:11 UTC