BUG: problems installing port coq when lablgtk2 port is present

[diem@…]

I tried to

sudo port install coq

but I get the error message as shown below.

(I first did both sudo port -d selfupdate, and sudo port -d sync.)

With coq version 8.0pl2, coqide use to work just fine ...

Any help or suggestions would be appreciated, Dimitri

$ sudo port install coq

---> Building coq with target world Error: Target com.apple.build returned: shell command "cd "/opt/local/var/db/dports/build/_opt_local_var_db_dports_sources_rsync.rsync.darwinports.org_dpupdate_dports_lang_coq/work/coq-8.0pl3" && make world" returned error 2 Command output: File "ide/coqide.ml", line 2780, characters 6-15: Warning Y: unused variable compile_m. File "ide/coqide.ml", line 2373, characters 6-18: Warning Y: unused variable edit_prefs_m. File "ide/coqide.ml", line 2279, characters 6-17: Warning Y: unused variable find_back_i. File "ide/coqide.ml", line 2275, characters 6-12: Warning Y: unused variable find_i. File "ide/coqide.ml", line 2123, characters 6-26: Warning Y: unused variable case_sensitive_check. File "ide/coqide.ml", line 2113, characters 6-17: Warning Y: unused variable replace_lbl. File "ide/coqide.ml", line 2103, characters 6-14: Warning Y: unused variable find_lbl. File "ide/coqide.ml", line 2036, characters 6-12: Warning Y: unused variable quit_m. File "ide/coqide.ml", line 2003, characters 6-17: Warning Y: unused variable export_ps_m. File "ide/coqide.ml", line 2000, characters 6-18: Warning Y: unused variable export_dvi_m. File "ide/coqide.ml", line 1997, characters 6-20: Warning Y: unused variable export_latex_m. File "ide/coqide.ml", line 1994, characters 6-19: Warning Y: unused variable export_html_m. File "ide/coqide.ml", line 1963, characters 6-13: Warning Y: unused variable print_m. The files /opt/local/lib/ocaml/threads/thread.cmi and /opt/local/lib/ocaml/lablgtk2/gtkThread.cmi make inconsistent assumptions over interface Thread make: * [ide/coqide.cmo] Error 2

Error: /opt/local/bin/port: Status 1 encountered during processing.

[reilles@…]

I did not have this problem, since i don't have lablgtk2 installed. In you case, coq's configure detected lablgtk2, and thus tried to build coqide

I think this is a flaw in darwinports: coq should not try to link against lablgtk2 unless being told to, this makes many packages builds quite non deterministic.

It looks like your lablgtk2 needs to be updated, for coqide to be built. the "Y" warnings are easy to fix, you just have to replace those variables by _, or remove the "let" defining them. the lablgtk2 problem may be more complex

[reilles@…]

Maybe simply rebuilding lablgtk2 may be enough to get rid of the problem

[markd@…]

This behavior is because of the configure script. You could add a +lablgtk2 variant and patch the configure script to not install support for lablgtk2 unless the variant were used. If the variant were used it would also install lablgtk2 before coq as a dependency. Better yet, make a patch to add configure switches and send them to the developers, or ask the developers to add them such as --without-liblgtk2. This would make it a trivial matter to control whether coq builds with or without liblgtk2. The work is in the configure script, the rest is easy.

[jmroot (Joshua Root)]

Does this problem still occur?

[jmroot (Joshua Root)]

Reporter mailed me privately and indicated that the problem no longer occurs. Marking fixed.

[(none)]

Milestone Port Bugs deleted