Opened 10 years ago

Closed 10 years ago

Last modified 10 years ago

#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)

main.log.gz (11.7 KB) - added by lord@… 10 years ago.
patch-kernel-univ.ml.diff (397 bytes) - added by pmetzger (Perry E. Metzger) 10 years ago.
patch file to be placed in files/ subdir
Portfile.diff (677 bytes) - added by pmetzger (Perry E. Metzger) 10 years ago.
patch for Portfile

Download all attachments as: .zip

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

Cc Me!

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).

  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)
  1. 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: newassigned
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: assignedclosed

Thanks! r127095

comment:11 Changed 10 years ago by lord@…

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

comment:12 Changed 10 years ago by lord@…

It is already available. Built and installed. Thanks!

Note: See TracTickets for help on using tickets.