Isabelle2016与证明通用

Question

我一直在努力学习如何利用2016年伊莎贝尔。虽然原则上我喜欢异步验证检查的想法，但我不喜欢Isabelle/jEdit，原因很多，其中最严重的原因是它占用了太多内存(对我来说)。

如果我能和2016年伊莎贝尔一起使用好的老证据将军，那就太好了。我将变量isa-isabelle-command设置为指向伊莎贝尔分发目录下的文件bin/isabelle。当我使用C-g的菜单启动Isabelle时，Emacs会挂起，当我通过C-g中断它时，我会在*isabelle*缓冲区中得到以下内容。

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

我知道在这个网站上有一些旧的帖子，其中建议移除伊莎贝尔这个证明一般用来与定理证明器通信的组件。对于2016年的伊莎贝尔来说，这仍然是真的吗？我怎么能用最新版本的伊莎贝尔来使用“证明通用”呢？

Answer 1

是的，它仍然是真的；它还没有被重新引入。我不可能在2014年以后和伊莎贝尔一起执教皮卡。来自NEWS of Isabelle2015：

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

Answer 2

问题应该在实际发生的地方得到解决。Isabelle2016中的Prover所需的资源再次减少--这是近年来的一个共同主题。当证据将军在1998年出现时，它确实是巨大的和肥胖的时代。相比之下，Isabelle/jEdit相当轻巧:它应该在只有8GB内存的普通消费机器上平稳工作。

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