Opened 15 years ago

Closed 15 years ago

#22205 closed defect (fixed)

coq-8.2pl1 +coqide build failure.

Reported by: aran@… Owned by: reilles@…
Priority: Normal Milestone:
Component: ports Version: 1.8.1
Keywords: coqide Cc:
Port: coq

Description

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.

Change History (8)

comment:1 Changed 15 years ago by aran@…

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

comment:2 Changed 15 years ago by mf2k (Frank Schima)

Keywords: coq removed
Owner: changed from macports-tickets@… to reilles@…

comment:3 Changed 15 years ago by 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

comment:4 Changed 15 years ago by 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.

comment:5 Changed 15 years ago by 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).

comment:6 Changed 15 years ago by 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.

comment:7 Changed 15 years ago by 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.

comment:8 Changed 15 years ago by avsm@…

Resolution: fixed
Status: newclosed

confirmed fixed in -current macports with the lablgtk2 change

Note: See TracTickets for help on using tickets.