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
Last updated: Jul 10 2026 at 17:48 UTC