Coqide錯誤：編譯庫Basics.vo在庫上做出不一致的假設

Question

我在Mac OS X上使用CoqIDE_8.4pl5。 當CoqIDE轉發到此命令時，彈出此錯誤消息：要求導入基礎。

錯誤：編譯庫Basics.vo使得不一致的假設在圖書館 Coq.Init.Notations

我使用CoqIDE_8.4pl5時，我沒有得到我的舊的Macbook Air這個問題，但是，當我一個新的MacBook Pro，我從同一個網站再次下載它。 但是這次在這個macbook pro上，我用brew木桶安裝coq來安裝它......但它似乎不起作用，所以我從網站上下載它並將我的coqide路徑設置爲它在我的舊版macbook空氣..當我嘗試轉發我的任務，我得到這個問題。有沒有什麼辦法解決這一問題？或者我必須刪除coq並複製並重新安裝它？

Answer 1

這通常是Coq的一種情況，告訴您Basics.v（Basics.vo）的編譯版本已使用與當前正在使用的版本不同的Coq版本編譯。

出於安全原因，每個版本的Coq只想使用使用同一版本編譯的文件。

該修復通常是刪除導致Basics.vo文件並重現創建它的編譯步驟。

如果錯誤再次發生，則可能是您的系統安裝了兩個版本的Coq，其中一個由您的構建腳本訪問，另一個由CoqIDE使用。