4

I got the same error as from this question: Coqide Error: Compiled library Basics.vo makes inconsistent assumptions over library

Error:
Compiled library my_bool (in file /Users/Satan/lf_Satan/my_bool.vo) makes inconsistent assumptions over library Coq.Init.Logic

the question & answer I linked explain that the error is due to mismatching version of Coq. I have no idea why I have mismatching version of Coq. I am trying to compile something in the terminal while I am developing in Proof General. Might that be the mismatch of version?

Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
  • [Here's](https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:exn.compiled-library-ident-vo-makes-inconsistent-assumptions-over-library-qualid) the error in the reference manual. For what it's worth, if I use the wrong version of the Coq compiler I usually get the error right below that one - "Bad magic number" - rather than complaints about inconsistent assumptions. – SCappella Jan 10 '19 at 06:44
  • The answer to your question depends on your setup. As an opam user, I usually change to the right Coq version from within Emacs using the following https://gist.github.com/anton-trunov/b55fae56f92c35531fc480232bc74160 elisp snippet (`M-x coq-change-compiler`). The snippet is still not finished and has some quirks, so any patches improving it are very welcome. HTH – Anton Trunov Jan 10 '19 at 08:27
  • @AntonTrunov Anton, what information do I need to provide to get help with this? What commands would I run to show this information? – Charlie Parker Jan 16 '19 at 23:40
  • @Pinocchio You can first check that you see the same version of Coq from Proof General (PG) and your terminal. Try `Print LoadPath` or something like `Locate File "Init.vo".` in PG to determine which Coq is used by PG. From your terminal, `which coqc` or `where coqc` will tell you which Coq you're using in your terminal. If the versions are the same, I think we need more information about your project (the list of .v files, a description of what command you use in your terminal, ...). – eponier Jan 17 '19 at 10:25
  • @eponier how do I run `Print LoadPath` or check the version of Coq in Proof General (PG)? For my terminal one I have `$ which coqc /usr/local/bin/coqc` – Charlie Parker Jan 18 '19 at 22:07
  • 1
    `Print LoadPath.` is a standard vernacular command of Coq. Just type it in PG and validate it like any other instruction. It should show a list of directories with a common prefix. This prefix is where Coq (the one seen from PG) is installed. – eponier Jan 21 '19 at 08:50
  • related: https://stackoverflow.com/questions/54394510/how-does-one-switch-to-a-specific-version-of-coq – Charlie Parker Jun 08 '22 at 18:26

0 Answers0