证明如果同时运行2个脚本，则一般抱怨脚本不完整

似乎PG不允许同时运行2个脚本。在尝试这样做的那一刻，Emacs会提示并要求撤消另一个文件。有时候，脚本不会重新运行。有没有办法在单个Emacs实例中真正运行2个（或更多）脚本？我认为coqide gui没有coq没有这样的问题。证明如果同时运行2个脚本，则一般抱怨脚本不完整

2017-09-02 HuStmpHrrr

目前版本的PG似乎不可能。下面是从Proof General manual的摘录：

但是，你不能有一个以上的缓冲区，其中仅证明脚本的一小部分包含一个锁定的区域。在另一个校验脚本缓冲区中使用脚本管理之前，您必须完全断言或收回当前的脚本缓冲区。

2017-09-02 20:01:01

是的，我也看到了。我不确定我是否明白为什么会存在这样的限制，并且文档中的解释还不够清楚。我认为这可能是由于在后台运行的只有一个coqtop实例，并且似乎不可能提高进程的数量。你有什么机会有一些见解？ – HuStmpHrrr

看到我的答案。问题在于，证明将军对全球变量有着不幸的依赖。 – Perry

我的理解是，目前的Proof General有太多的全局变量在使用，以允许同时执行多个脚本实例。显然有一些工作正在通过封装全球状态来解决这个问题，但我不知道什么时候可以完成。

2017-09-02 22:57:47 Perry

回答