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

Answer 1

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

出于安全原因,每个版本的Coq只想使用使用相同版本编译的文件.

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

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