The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

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