6

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

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

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

我知道该站点上的旧帖子表明 Proof General 用于与定理证明器通信的 Isabelle 组件已被删除。2016 年的伊莎贝尔 (Isabelle) 是否（仍然）如此？如何在新版本的 Isabelle 中使用 Proof General？

4

2 回答 2

6

是的，它仍然是真的；它没有被重新引入。我不知道在 2014 年之后与 Isabelle 一起运行 PG。从NEWSIsabelle2015 开始：

* Support for Proof General and Isar TTY loop has been discontinued.
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
于 2016-02-22T06:24:43.830 回答
1

问题应该在实际发生的地方解决。Isabelle2016 中的 Prover IDE 再次需要更少的资源——这是近年来的一个共同主题。当 Proof General 于 1998 年问世时，它在当时确实是巨大而肥大的。相比之下，Isabelle/jEdit 相当轻巧：它应该可以在只有 8 GB 内存的普通消费类机器上顺利运行。

您可能使用的是 Linux x86_64 并且没有安装Isabelle安装页面上提到的32 位 C/C++ 标准库。忽略这一点，会使 ML 堆需求翻倍而没有任何好处。

于 2016-03-01T15:44:41.420 回答