Coqide错误:编译库Basics.vo对库做了不一致的假设

Question

我在mac上使用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只想使用用相同版本编译的文件。

修复方法通常是删除牵连的Basics.vo文件，并重新执行创建该文件的编译步骤。

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