Search code examples
emacsisabelle

How can I use Isabelle in Emacs


Most of the Isabelle documentation I see says that Proof-General supports Isabelle, but as far as I know PG dropped support about 5 years ago.

Is there another possibility to use (current) Isabelle with Emacs? Neither JEdit, nor VSCode really work for me.


Solution

  • There is no official solution and no way to make Proof General work again.

    However, there is an unofficial solution. You could try isabelle-emacs (Disclaimer: I develop it in my free time. The experience is a bit rough, but there are a few people using it). It uses the Isabelle's LSP server like VScode, but it uses Emacs based. The difference between isabelle-emacs and Isabelle is limited to a few line in the LSP server and the Emacs specific code. Neither kernel nor any other theory is changed.