emacs - 如何在 Emacs 中使用 Isabelle

Question

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

是否有另一种可能将（当前）Isabelle 与 Emacs 一起使用？JEdi​​t 和 VSCode 都不适合我。

标签： emacsisabelle

Answer 1

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

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