Isabelle2016和证明一般

Question

我一直在努力学习虽然原则上我喜欢异步防爆检查的主意,用伊莎贝尔2016年,我不喜欢伊莎贝尔/ 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组件被删除了.这是(仍然)Isabelle 2016的真实情况吗？如何在较新版本的Isabelle中使用Proof General？

Answer 1

是的,它仍然是真的; 它还没有被重新引入.我不知道在2014年之后与Isabelle一起运行PG.来自NEWSIsabelle2015:

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