The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

You're talking about a "new local installation". Did you use option
"-local" at configure time? If not, coq is not supposed to work
properly until "make install" is done.

Alternatively, you can add option

  "-coqlib /Users/gaspar/Downloads/coq-8.4/"

to coqtop to force the use of your local installation directory (in
place of the expected installation repository).

Hugo Herbelin

On Tue, Nov 20, 2012 at 05:17:45PM +0100, Nuno Gaspar wrote:
> 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.