Coqide 错误 : Compiled library 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 cask install coq 来安装它......但它似乎不起作用，所以我从网站下载了它并将我的 coqide 路径设置为与我的旧 macbook 中的路径相同空气..当我尝试转发我的作业时，我遇到了这个问题。有没有什么办法解决这一问题？或者我是否必须删除 coq 并复制并重新安装它？

Answer 1

这通常是 Coq 告诉您 Basics.v (Basics.vo) 的编译版本是使用与您当前使用的 Coq 版本不同的 Coq 版本编译的。

出于安全原因，Coq 的每个版本只希望使用用同一版本编译的文件。

修复方法通常是删除有罪的 Basics.vo 文件并重现创建它的编译步骤。

如果错误再次发生，则可能是您的系统安装了两个版本的 Coq，其中一个版本由您的构建脚本访问，而另一个版本由 CoqIDE 使用。