coq-8.2pl1 +coqide build failure.

[aran@…]

I am not able to build coq with coqide. I have installed lablgtk2 without problem. I even tried modifying the port file to use the "byte" option for building coqide instead of "opt."

I receive the following error:

bash-3.2$ sudo port clean coq
Password:
--->  Cleaning coq
bash-3.2$ sudo port install coq +coqide
--->  Computing dependencies for coq

<snip>

--->  Building coq
Error: Target org.macports.build returned: shell command " cd "/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_ports_lang_coq/work/coq-8.2pl1" && /usr/bin/make -j1 world " returned error 2
Command output: OCAMLC    ide/utils/configwin.ml

<snip>

OCAMLC    ide/coqide.mli
OCAMLC    ide/coqide.ml
OCAMLC -a -o ide/ide.cma
COQMKTOP -o bin/coqide.byte
File "/tmp/coqmaind0ab92.ml", line 1, characters 0-1:
Error: The file /opt/local/lib/ocaml/lablgtk2/gtkThread.cmo is not a bytecode object file
make[1]: *** [bin/coqide.byte] Error 2
make: *** [world] Error 2

Error: Status 1 encountered during processing.

[aran@…]

After much trial and error, uninstalling and reinstalling lablgtk2 before installing coq seemed to do the trick.

[kiyoshi.coquser@…]

Please show us the details about your environment.

uname -a; sw_vers; xcodebuild -version; port version; ocaml -version; file /opt/local/lib/ocaml/lablgtk2/gtkThread.cmo

[aran@…]

~ aran$ uname a; sw_vers; xcodebuild -version; port version; ocaml -version; file /opt/local/lib/ocaml/lablgtk2/gtkThread.cmo usage: uname [-amnprsv] ProductName: Mac OS X ProductVersion: 10.5.8 BuildVersion: 9L30 Xcode 3.1.3 Component versions: DevToolsCore-1192.0; DevToolsSupport-1186.0 BuildVersion: 9M2736 Version: 1.8.1 The Objective Caml toplevel, version 3.11.1 /opt/local/lib/ocaml/lablgtk2/gtkThread.cmo: Objective caml object file (.cmo) (Version 007).

Like I mentioned, removing and reinstalling lablgtk2 allowed me to install coqide, so I'm not sure I can get my system back into the erroneous state... sorry.

[aran@…]

Once more, with wiki formatting.

~ aran$ uname a; sw_vers; xcodebuild -version; port version; ocaml -version; file /opt/local/lib/ocaml/lablgtk2/gtkThread.cmo
usage: uname [-amnprsv]
ProductName:	Mac OS X
ProductVersion:	10.5.8
BuildVersion:	9L30
Xcode 3.1.3
Component versions: DevToolsCore-1192.0; DevToolsSupport-1186.0
BuildVersion: 9M2736
Version: 1.8.1
The Objective Caml toplevel, version 3.11.1
/opt/local/lib/ocaml/lablgtk2/gtkThread.cmo: Objective caml object file (.cmo) (Version 007).

[kiyoshi.coquser@…]

Thanks aran.

Probably gtkThread.cmo file was broken.

I guess that parallel building of lablegtk2 occasionally emits such broken files.

Adding "use_parallel_build no" line to Portfile of lablgtk2 will fix this issue.

[kiyoshi.coquser@…]

Lablgtk2 port is updated from 2.10.1 to 2.14.0 with "use_parallel_build no" at #22314 .

So we can build Coq without error like this report, now.

[avsm@…]

confirmed fixed in -current macports with the lablgtk2 change