The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,
On the one hand, Coq 8.3pl4 does not compile with Ocaml4. Coq 8.3 svn branch 
does so you can use it.

On the other hand, being able to use directly the binaries in Resources/bin/ 
of my bundles relies on the fact these binaries look for the standard library 
in a relative place from themselves (vs the absolute path given at configure 
time). It is true only in >= v8.4 Consequently, you'll have to do 
 /Applications/CoqIdE_8.3pl4.app/Contents/Resources/bin/coqtop -coqlib 
/Applications/CoqIdE_8.3pl4.app/Contents/Resources/lib/coq

Pierre B.

Le 24 sept. 2012 à 15:52, Andrej Bauer 
<andrej.bauer AT andrej.com>
 a écrit :

> The current version of coq in mac ports has a problem (Mountain Lion,
> Mac Ports upgraded): port install coq starts compiling coq 8.3pl4 and
> dies with the error:
> 
>  make[1]: *** No rule to make target `lib/pp.ml4.ml.d', needed by
> `lib/pp.cmx'.  Stop.
> 
> Then when I try to compile it by hand from sources, configure tells me
> 
>  You have Objective-Caml 4.00.0. Good!
>  Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3,
>  only the bytecode version of Coq will be available.
> 
> What's up with that? I thought 4.00 >= 3.09.3.
> 
> Then if I install the .dmg file, coqtop tells me this:
> 
> $ /Applications/CoqIdE_8.3pl4.app/Contents/Resources/bin/coqtop
> Welcome to Coq 8.3pl4 (March 2012)
> Error during initialization:
> Error: File /usr/local/lib/coq/states/initial.coq has bad magic number. It 
> is
> corrupted or was compiled with another version of Coq.
> 
> Why is it looking in /usr/local? It is installed in /Applications, it
> has no business looking there. At least that's how it usually goes
> with Mac applications. (There is Coq 8.4 in /usr/local, it compiles
> fine from the source.)
> 
> I'd be happies if there was a fix for the port version, or the
> hand-compiled one. I understand that I can get rid of Coq 8.4 to run
> Coq 8.3 from /Applications, but that seems silly. Please help!
> 
> With kind regards,
> 
> Andrej