coq @8.4pl4_0: build fails due to stricter OCaml compiler

[lord@…]

Trying to install coq @8.4pl4 under MacOS 10.10. Using XCode 6.1. Build fails. Log file is attached. Trying to run failed command manually gives the following error:

make: Entering directory `/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl4'
/Applications/Xcode.app/Contents/Developer/usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build "world"
make[1]: Entering directory `/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl4'
OCAMLC    kernel/univ.ml
OCAMLC    kernel/esubst.ml
OCAMLC    kernel/term.mli
OCAMLC    interp/ppextend.ml
OCAMLC    parsing/lexer.mli
OCAMLC    parsing/extend.ml
File "kernel/univ.ml", line 229, characters 0-2:
Error: This comment contains an unterminated string literal
File "kernel/univ.ml", line 229, characters 17-20:
Error: String literal begins here
make[1]: *** [kernel/univ.cmo] Error 2
make[1]: *** Waiting for unfinished jobs....
File "kernel/esubst.ml", line 52, characters 23-24:
Warning 3: deprecated: Pervasives.&
Use (&&) instead.
make[1]: Leaving directory `/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl4'
make: *** [world] Error 2
make: Leaving directory `/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl4'

[lord@…]

Cc Me!

[lord@…]

For those of us who left without working COQ installation while this is being fixed here is a workaround. (Assuming you are using Proof General and do not need COQIDE).

1. Download and install binary COQ from ​http://coq.inria.fr/download (Do not try to run it, it would not start. This is a separate issue)

2. Add /Applications/CoqIde_8.4pl4.app/Contents/Resources/bin/ to your shell path $PATH

This would allow you to run COQ from Proof General.

[pmetzger (Perry E. Metzger)]

I'm on it, will try to reproduce as soon as macports on my Yosemite machine is up to date.

[pmetzger (Perry E. Metzger)]

I have found the problem -- succinctly, it isn't a Yosemite problem, but rather that a newer OCaml compiler has become stricter about the contents of comments. See:

​http://caml.inria.fr/mantis/view.php?id=6561

The problem is actually kind of ridiculous. If you don't want to wait for me to get the patch in, just edit line 229 of kernel/univ.ml temporarily -- you can even remove the comment if you like.

[pmetzger (Perry E. Metzger)]

patch file to be placed in files/ subdir

[pmetzger (Perry E. Metzger)]

patch for Portfile

[pmetzger (Perry E. Metzger)]

Okay, I've created the needed patches, I'll get someone to apply them.

[lord@…]

Thanks for looking into that. I will wait for patches to make into repository and will try to reinstall then.

[larryv (Lawrence Velázquez)]

Thanks! r127095

[lord@…]

Thanks! When this would be visible in ports tree (via 'port update')?

[lord@…]

It is already available. Built and installed. Thanks!