證明如果同時運行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

回答