9

i'm using CoqIDE_8.4pl5 on mac os X. This error message pops up when CoqIDE forwards to this command: Require Import Basics.

Error: Compiled library Basics.vo makes inconsistent assumptions over library Coq.Init.Notations

I didn't get this problem on my old Macbook Air when i was using CoqIDE_8.4pl5, but when i got a new macbook pro, and i downloaded it again from the same website. But this time on this macbook pro, i used brew cask install coq to get it installed... but it seemed to not work, so i downloaded it from the website and set my coqide path to the same path it was in my old macbook air.. and when i try forwarding my assignments, i get this problem. Is there anyway to fix this? or do i have to remove coq and copied and reinstall it?

pheonixkid
  • 101
  • 1
  • 5
  • how did you make sure that everything was using the right version of Coq when you compiled? Did you try this in proof general? – Charlie Parker Jan 10 '19 at 03:53

1 Answers1

9

This is usually a case of Coq telling you that the compiled version of Basics.v (Basics.vo) has been compiled with a different version of Coq than the one you are currently using.

For safety reasons, each version of Coq only wants to use files compiled with that same version.

The fix is usually to delete the incriminating Basics.vo file and reproduce the compilation step that created it.

If the error happens again, then it might be a case of your system having two versions of Coq installed, one of which is reached by your building script, while the other one is use by CoqIDE.

Ptival
  • 9,167
  • 36
  • 53
  • How do you recompile the Coq code so that it works? I am having this issue but with proof general. – Charlie Parker Jan 10 '19 at 03:47
  • It depends on a lot on the setup of the project. You might want to run something like `make` from the project directory. I seem to recall some setup in which ProofGeneral would compile files for you, but I don't remember how to make it happen... Reading the README for your particular project can help. If the project has a `_CoqProject` file, you should be able to `coq_makefile -f ./_CoqProject -o Makefile`, and then run `make`, for instance. – Ptival Jan 10 '19 at 18:13