似乎 PG 不允许同时运行 2 个脚本。尝试执行此操作的那一刻，Emacs 将提示并要求收回另一个文件。有时，重新运行脚本并非易事。有没有办法在单个 Emacs 实例中实际运行 2 个（或更多）脚本？我不认为 coq 附带的 coqide gui 没有这样的问题。
问问题
123 次
2 回答
2
当前版本的 PG 似乎不可能。以下是Proof General 手册的摘录：
但是，您不能拥有多个缓冲区，其中只有一小部分证明脚本包含锁定区域。在您可以在另一个证明脚本缓冲区中使用脚本管理之前，您必须完全断言或收回当前脚本缓冲区。
于 2017-09-02T20:01:01.273 回答
1
我的理解是，当前的 Proof General 使用的全局变量太多，无法同时执行多个脚本实例。显然有一些工作正在进行中，通过封装全局状态来解决这个问题，但我不知道什么时候可以完成。
于 2017-09-02T22:57:47.367 回答