The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello.

I just successfully installed coq-8.4 on ./bin and wanted to try it on my development in which I've been using a pior version of Coq.  Essentially, I just wanted to have a feeling of what I will need to change before fully installing (sudo make install) coq-8.4 on my machine.

I tried to run coq-8.4 but got the following error:

Connection with coqtop failed!

Command was: '/Users/gaspar/Downloads/coq-8.4/bin/coqtop' -batch 

Answer was: Welcome to Coq 8.4 (November 2012)

  Error: File /usr/local/lib/coq/states/initial.coq has bad magic number. It is

  corrupted or was compiled with another version of Coq.

Exception was: Coq.WrongExitStatus("WEXITED 1")

I know that this 'bad magic number' error message arises whenever we try to use different versions of Coq, but in this case I don't understand where is the problem. 

Why couldn't I have an old version of Coq (fully) installed and be able to run a new local installation of a newer one? Or by other words, why does starting coq-8.4 depends on /usr/local/lib/coq/states/initial.coq anyway? 

Any ideas on how to fix this ?

Thank you :-)

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.