如何在Emacs中使用Isabelle

Question

我看到的大多数Isabelle文档都说Proof-General支持Isabelle，但据我所知，PG在大约5年前就放弃了支持。

是否有其他可能将(当前的) Isabelle与Emacs一起使用？JEdit和VSCode都不适合我。

Answer 1

没有官方的解决方案，也没有办法让Proof General再次工作。

然而，有一个非官方的解决方案。你可以试试isabelle-emacs (免责声明:我是在空闲时间开发的。体验有点粗糙，但也有一些人在使用它)。它使用Isabelle的LSP服务器，比如VScode，但它使用基于Emacs的服务器。isabelle-emacs和Isabelle之间的区别仅限于LSP服务器和Emacs特定代码中的几行。内核和任何其他理论都没有改变。