Email Gateway (Jun 03 2025 at 20:00): Email Gateway (Jun 03 2025 at 20:00):From: Humam Alhusaini via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Hello, hope you all are doing well.
I'd like to create a Neovim plugin that is essentially Coqtail (https://github.com/whonore/coqtail) but for Isabelle. According to a blog post (https://whonore.github.io/src/projects/coqtail.html), Coqtail uses Coq's XML protocol to function, which is well documented here (https://github.com/rocq-prover/rocq/blob/master/dev/doc/xml-protocol.md). As far as I know, there isn't much documentation on how to communicate with Isabelle/PIDE, though I believe that the way to do it would be through XML, as I see some use of the XML protocol in the Isabelle code I downloaded. I can't really tell if what I want to do is possible without significant changes to Isabelle itself, so I'm asking for the opinion of somebody who knows what they are doing.
Thank you for reading this, hope you have a great day.
Email Gateway (Jun 04 2025 at 07:51):From: Fabian Huch <huch@in.tum.de>
On 6/3/25 21:59, Humam Alhusaini via isabelle-dev wrote:
I'd like to create a Neovim plugin
That already exists [1].
there isn't much documentation on how to communicate with
Isabelle/PIDE, though I believe that the way to do it would be through XML
The important question here is the protocol; wire formats are easily
interchangeable. We use LSP with PIDE extensions for such experiments.
Fabian
[1]: https://github.com/Treeniks/isabelle-lsp.nvim
Last updated: Jul 12 2025 at 16:25 UTC