The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

On Fri, Mar 26, 2010 at 8:06 AM, Tom Hutchinson
<thomas.hutchinson AT sophia.inria.fr>
 wrote:
> Was your lablgtk2 installed with an rpm (or manually by source)?
>
> If it's an rpm, then maybe you need to install lablgtk2-devel. (I don't 
> know much about OpenSUSE so it's just a guess)
>
> I compiled CoqIDE with lablgtk2 2.14.0. Still, the file /ide/utils/okey.ml 
> hasn't been changed in years. I would be surprised if it required a really 
> recent lablgtk version.
>
> http://docs.camlcity.org/docs/godipkg/3.10/godi-lablgtk2/lib/ocaml/pkg-lib/lablgtk2/gdk.mli
> It looks like there is a Gdk.Tags.modifier
> This is from 2.12.0 (see bottom: 
> http://docs.camlcity.org/docs/godipkg/3.10/godi-lablgtk2)

CoqIDE(8.2pl1 and 8.3) was finally installed on openSUSE 11.2. In case
someone else needs it:

First installed lablgtk2-devel, the latest version from YaST2 is
12.0.1. Then the errors from
/ide/utils/okey.mli were gone. But then there was another linkage
error, about 'cannot find
dlllablgtk2.so', which was also reported at
'http://logical.saclay.inria.fr/coq-puma/messages/619bff6dadbe2454'.

Followed that suggestion,
1. make distclean
2. ./configure -coqrunbyteflags -custom <whatever-options-you-want>
3. make
that linkage error was fixed. Then, more linkage errors:
1) cannot find ncurses --> the dev-ncurses should also be installed
2) could not find gtk-x11-2.0
    this was fixed by sudo ln -s gtk-x11-2.0.so.1 gtk-x11-2.0.so
3) make softlinks at /usr/lib for the following libs too
    gtk-x11-2.0 gdk-x11-2.0 atk-1.0 gio-2.0 pangoft2-1.0
gdk_pixbuf-2.0 gobject-2.0 pangocairo-2.0 cairo pango-1.0 freetype
fontconfig gmodule glib-2.0

This completes the installation.

A dev-version of lablgtk2 provides dlllablgtk2.so
http://rpm.pbone.net/index.php3/stat/4/idpl/11743232/com/lablgtk-2.12dev-13.1.i386.rpm.html
I guess this can fix the problem too, but it works if frama-c is
installed, and has other dependencies.

>
> Tom
>
> On Mar 26, 2010, at 12:04 AM, Jianzhou Zhao wrote:
>
>> Hi,
>>
>> I got the error when compiling 8.3:
>>
>> ./ide/utils/okey.mli line 33
>> Unbound type constructor Gdk.Tags.modifier
>>
>> This seems a problem from Lablgtk2:
>> http://caml.inria.fr/pub/ml-archives/ocaml-beginners/2004/01/c57a676198b126994795763abf5ad5b1.en.html
>>
>> I used
>>  Camlp5 version 5.13 (ocaml 3.11.0)
>>  Lablgtk2 with 2.12.0
>>  OpenSUSE 11.2
>> What is the correct Lablgtk2 CoqIDE needs?
>>
>> I remember I had the same problem when I compiled 8.2 last year,
>> and commented CoqIDE compilations.
>>
>> Thanks
>> --
>> Jianzhou
>
>



-- 
Jianzhou