Isabelle2016 和 Proof General
Isabelle2016 and Proof General
我一直在尝试学习使用 Isabelle 2016。虽然原则上我喜欢异步验证检查的想法，但出于多种原因我不喜欢 Isabelle/jEdit，其中最严重的是它占用了太多内存（对我来说）。
如果我能在 Isabelle 2016 中使用旧的 Proof General 就好了。我设置变量 isa-isabelle-command 以指向 Isabelle 分发目录下的文件 bin/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 一起使用？
是的，还是这样；它没有被重新引入。据我所知，在 2014 年以后 运行 与 Isabelle 的 PG 是不可能的。来自 Isabelle2015 的 NEWS：
* Support for Proof General and Isar TTY loop has been discontinued.
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
有问题就在实际发生的地方解决。 Isabelle2016 中的 Prover IDE 再次需要更少的资源——这是近年来的一个共同主题。当 Proof General 于 1998 年问世时，它在当时确实又大又胖。相比之下 Isabelle/jEdit 相当轻巧：它应该可以在只有 8 GB 内存的普通消费类机器上流畅运行。
您可能正在使用 Linux x86_64 并且没有安装 32 位 C/C++ 标准库如 Isabelle installation 页面所述。忽略这一点，将 ML 堆要求加倍而没有任何好处。
我一直在尝试学习使用 Isabelle 2016。虽然原则上我喜欢异步验证检查的想法，但出于多种原因我不喜欢 Isabelle/jEdit，其中最严重的是它占用了太多内存（对我来说）。
如果我能在 Isabelle 2016 中使用旧的 Proof General 就好了。我设置变量 isa-isabelle-command 以指向 Isabelle 分发目录下的文件 bin/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 一起使用？
是的，还是这样；它没有被重新引入。据我所知，在 2014 年以后 运行 与 Isabelle 的 PG 是不可能的。来自 Isabelle2015 的 NEWS：
* Support for Proof General and Isar TTY loop has been discontinued.
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
有问题就在实际发生的地方解决。 Isabelle2016 中的 Prover IDE 再次需要更少的资源——这是近年来的一个共同主题。当 Proof General 于 1998 年问世时，它在当时确实又大又胖。相比之下 Isabelle/jEdit 相当轻巧：它应该可以在只有 8 GB 内存的普通消费类机器上流畅运行。
您可能正在使用 Linux x86_64 并且没有安装 32 位 C/C++ 标准库如 Isabelle installation 页面所述。忽略这一点，将 ML 堆要求加倍而没有任何好处。