#45508 closed defect (fixed)
coq @8.4pl4_0: build fails due to stricter OCaml compiler
Reported by: | lord@… | Owned by: | larryv (Lawrence Velázquez) |
---|---|---|---|
Priority: | Normal | Milestone: | |
Component: | ports | Version: | 2.3.2 |
Keywords: | Cc: | pmetzger (Perry E. Metzger) | |
Port: | coq |
Description
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'
Attachments (3)
Change History (15)
Changed 10 years ago by lord@…
Attachment: | main.log.gz added |
---|
comment:1 Changed 10 years ago by lord@…
Cc: | lord@… added |
---|
comment:2 Changed 10 years ago by 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).
- 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)
- Add /Applications/CoqIde_8.4pl4.app/Contents/Resources/bin/ to your shell path $PATH
This would allow you to run COQ from Proof General.
comment:3 Changed 10 years ago by ryandesign (Ryan Carsten Schmidt)
Cc: | lord@… removed |
---|---|
Keywords: | coq removed |
Owner: | changed from macports-tickets@… to perry@… |
comment:4 Changed 10 years ago by pmetzger (Perry E. Metzger)
I'm on it, will try to reproduce as soon as macports on my Yosemite machine is up to date.
comment:5 Changed 10 years ago by 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.
Changed 10 years ago by pmetzger (Perry E. Metzger)
Attachment: | patch-kernel-univ.ml.diff added |
---|
patch file to be placed in files/ subdir
Changed 10 years ago by pmetzger (Perry E. Metzger)
Attachment: | Portfile.diff added |
---|
patch for Portfile
comment:6 Changed 10 years ago by pmetzger (Perry E. Metzger)
Okay, I've created the needed patches, I'll get someone to apply them.
comment:7 Changed 10 years ago by larryv (Lawrence Velázquez)
Keywords: | yosemite removed |
---|---|
Owner: | changed from perry@… to larryv@… |
Status: | new → assigned |
Summary: | coq build fails on MacOS 10.10 (yosemite) → coq @8.4pl4_0: build fails due to stricter OCaml compiler |
comment:8 Changed 10 years ago by larryv (Lawrence Velázquez)
Cc: | perry@… added |
---|
comment:9 Changed 10 years ago by lord@…
Thanks for looking into that. I will wait for patches to make into repository and will try to reinstall then.
comment:10 Changed 10 years ago by larryv (Lawrence Velázquez)
Resolution: | → fixed |
---|---|
Status: | assigned → closed |
Thanks! r127095
comment:11 Changed 10 years ago by lord@…
Thanks! When this would be visible in ports tree (via 'port update')?
Cc Me!