Isabelle2016 和 Proof General

Question

我一直在尝试学习使用 Isabelle 2016。虽然原则上我喜欢异步证明检查的想法，但我不喜欢 Isabelle/jEdit 的原因有很多，其中最严重的是它使用了太多内存(为了我)。

如果我能在 Isabelle 2016 中使用旧的 Proof General 那就太好了。我设置了变量 isa-isabelle-command指向文件 bin/isabelle在 Isabelle 分发目录下。当我使用 Proof General 的菜单启动 Isabelle 时，Emacs 挂起，当我通过 C-g 中断它时, 我在 *isabelle* 中得到以下信息缓冲。

 > val it = (): unit
 ^BException- ERROR "Bad socket name: \"I\"" raised

我知道此站点上的旧帖子表明，Proof General 用来与定理证明者通信的 Isabelle 组件已被删除。 Isabelle 2016 是否(仍然)如此？如何将 Proof General 与较新版本的 Isabelle 一起使用？

Answer 1

是的，它仍然是正确的；它没有被重新引入。我不知道在 2014 年之后与 Isabelle 一起运行 PG。来自 NEWS Isabelle2015 的:

* Support for Proof General and Isar TTY loop has been discontinued.
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.