wanted to play with coq... emerge coq produces: [skipped...] OCAMLC ide/blaster_window.ml OCAMLC ide/undo.mli OCAMLC ide/undo.ml The implementation ide/undo.ml does not match the interface ide/undo.cmi: Class declarations do not match: class undoable_view : Gtk.text_view Gtk.obj -> object val redo : action Queue.t val obj : Gtk.text_view Gtk.obj val nredo : action Stack.t val history : action Stack.t method add_child_at_anchor : GObj.widget -> GText.child_anchor -> unit method add_child_in_window : child:GObj.widget -> which_window:Gtk.Tags.text_window_type -> x:int -> y:int -> unit method as_view : Gtk.text_view Gtk.obj method as_widget : Gtk.widget Gtk.obj method backward_display_line : GText.iter -> bool method backward_display_line_start : GText.iter -> bool method buffer : GText.buffer method buffer_to_window_coords : tag:Gtk.Tags.text_window_type -> x:int -> y:int -> int * int method clear_undo : unit method coerce : GObj.widget method connect : GText.view_signals method cursor_visible : bool method destroy : unit -> unit method drag : GObj.drag_ops method private dump_debug : unit method editable : bool method event : GObj.event_ops method forward_display_line : GText.iter -> bool method forward_display_line_end : GText.iter -> bool method get_border_window_size : [ `BOTTOM | `LEFT | `RIGHT | `TOP ] -> int method get_iter_at_location : x:int -> y:int -> GText.iter method get_iter_location : GText.iter -> Gdk.Rectangle.t method get_line_at_y : int -> GText.iter * int method get_line_yrange : GText.iter -> int * int method get_oid : int method get_window : Gtk.Tags.text_window_type -> Gdk.window option method get_window_type : Gdk.window -> Gtk.Tags.text_window_type method indent : int method justification : Gtk.Tags.justification method left_margin : int method misc : GObj.misc_ops method move_child : child:GObj.widget -> x:int -> y:int -> unit method move_mark_onscreen : GText.mark -> bool method move_visually : GText.iter -> int -> bool method pixels_above_lines : int method pixels_below_lines : int method pixels_inside_wrap : int method place_cursor_onscreen : unit -> bool method redo : bool method right_margin : int method scroll_mark_onscreen : GText.mark -> unit method scroll_to_iter : ?within_margin:float -> ?use_align:bool -> ?xalign:float -> ?yalign:float -> GText.iter -> bool method scroll_to_mark : ?within_margin:float -> ?use_align:bool -> ?xalign:float -> ?yalign:float -> GText.mark -> unit method set_border_window_size : typ:[ `BOTTOM | `LEFT | `RIGHT | `TOP ] -> size:int -> unit method set_buffer : GText.buffer -> unit method set_cursor_visible : bool -> unit method set_editable : bool -> unit method set_indent : int -> unit method set_justification : Gtk.Tags.justification -> unit method set_left_margin : int -> unit method set_pixels_above_lines : int -> unit method set_pixels_below_lines : int -> unit method set_pixels_inside_wrap : int -> unit method set_right_margin : int -> unit method set_wrap_mode : Gtk.Tags.wrap_mode -> unit method starts_display_line : GText.iter -> bool method undo : bool method visible_rect : Gdk.Rectangle.t method window_to_buffer_coords : tag:Gtk.Tags.text_window_type -> x:int -> y:int -> int * int method wrap_mode : Gtk.Tags.wrap_mode end does not match class undoable_view : Gtk.text_view Gtk.obj -> object val obj : [> Gtk.text_view ] Gtk.obj method add_child_at_anchor : GObj.widget -> GText.child_anchor -> unit method add_child_in_window : child:GObj.widget -> which_window:Gtk.Tags.text_window_type -> x:int -> y:int -> unit method as_view : Gtk.text_view Gtk.obj method as_widget : Gtk.widget Gtk.obj method backward_display_line : GText.iter -> bool method backward_display_line_start : GText.iter -> bool method buffer : GText.buffer method buffer_to_window_coords : tag:Gtk.Tags.text_window_type -> x:int -> y:int -> int * int method clear_undo : unit method coerce : GObj.widget method connect : GText.view_signals method cursor_visible : bool method destroy : unit -> unit method drag : GObj.drag_ops method editable : bool method event : GObj.event_ops method forward_display_line : GText.iter -> bool method forward_display_line_end : GText.iter -> bool method get_border_window_size : [ `BOTTOM | `LEFT | `RIGHT | `TOP ] -> int method get_iter_at_location : x:int -> y:int -> GText.iter method get_iter_location : GText.iter -> Gdk.Rectangle.t method get_line_at_y : int -> GText.iter * int method get_line_yrange : GText.iter -> int * int method get_oid : int method get_window : Gtk.Tags.text_window_type -> Gdk.window option method get_window_type : Gdk.window -> Gtk.Tags.text_window_type method indent : int method justification : Gtk.Tags.justification method left_margin : int method misc : GObj.misc_ops method move_child : child:GObj.widget -> x:int -> y:int -> unit method move_mark_onscreen : GText.mark -> bool method move_visually : GText.iter -> int -> bool method pixels_above_lines : int method pixels_below_lines : int method pixels_inside_wrap : int method place_cursor_onscreen : unit -> bool method redo : bool method right_margin : int method scroll_mark_onscreen : GText.mark -> unit method scroll_to_iter : ?within_margin:float -> ?use_align:bool -> ?xalign:float -> ?yalign:float -> GText.iter -> bool method scroll_to_mark : ?within_margin:float -> ?use_align:bool -> ?xalign:float -> ?yalign:float -> GText.mark -> unit method set_border_window_size : typ:[ `BOTTOM | `LEFT | `RIGHT | `TOP ] -> size:int -> unit method set_buffer : GText.buffer -> unit method set_cursor_visible : bool -> unit method set_editable : bool -> unit method set_indent : int -> unit method set_justification : Gtk.Tags.justification -> unit method set_left_margin : int -> unit method set_pixels_above_lines : int -> unit method set_pixels_below_lines : int -> unit method set_pixels_inside_wrap : int -> unit method set_right_margin : int -> unit method set_wrap_mode : Gtk.Tags.wrap_mode -> unit method starts_display_line : GText.iter -> bool method undo : bool method visible_rect : Gdk.Rectangle.t method window_to_buffer_coords : tag:Gtk.Tags.text_window_type -> x:int -> y:int -> int * int method wrap_mode : Gtk.Tags.wrap_mode end The instance variable obj has type ([> Gtk.text_view ] as 'a) Gtk.obj = 'a Gobject.obj but is expected to have type Gtk.text_view Gtk.obj = Gtk.text_view Gobject.obj Type 'a = [> `container | `gtk | `textview | `widget ] is not compatible with type Gtk.text_view = [ `container | `gtk | `textview | `widget ] make: *** [ide/undo.cmo] Error 2 !!! ERROR: sci-mathematics/coq-8.0-r1 failed. !!! Function src_compile, Line 65, Exitcode 2 !!! (no error message) !!! If you need support, post the topmost build error, NOT this status message. i've got many use flags due to "play-with-everything" experimental nature of installation: emerge info Portage 2.1_pre3-r1 (hardened/x86/2.6, gcc-3.4.5, glibc-2.3.6-r2, 2.6.15-suspend2-r3 i686) ================================================================= System uname: 2.6.15-suspend2-r3 i686 Intel(R) Pentium(R) 4 CPU 3.40GHz Gentoo Base System version 1.12.0_pre15 dev-lang/python: 2.3.5-r2, 2.4.2 sys-apps/sandbox: 1.2.17 sys-devel/autoconf: 2.13, 2.59-r7 sys-devel/automake: 1.4_p6, 1.5, 1.6.3, 1.7.9-r1, 1.8.5-r3, 1.9.6-r1 sys-devel/binutils: 2.16.1-r1 sys-devel/libtool: 1.5.22 virtual/os-headers: 2.6.11-r3 ACCEPT_KEYWORDS="x86 ~x86" AUTOCLEAN="yes" CBUILD="i686-pc-linux-gnu" CFLAGS="-O2 -march=pentium4 -fomit-frame-pointer" CHOST="i686-pc-linux-gnu" CONFIG_PROTECT="/etc /opt/openjms/config /usr/kde/2/share/config /usr/kde/3.5/env /usr/kde/3.5/share/config /usr/kde/3.5/shutdown /usr/kde/3/share/config /usr/lib/X11/xkb /usr/lib/mozilla/defaults/pref /usr/share/config /var/qmail/control" CONFIG_PROTECT_MASK="/etc/gconf /etc/init.d /etc/terminfo /etc/texmf/web2c /etc/env.d" CXXFLAGS="-O2 -march=pentium4 -fomit-frame-pointer" DISTDIR="/usr/portage/distfiles" FEATURES="autoconfig distlocks prelink sandbox sfperms strict" GENTOO_MIRRORS="/home/qwe/Network/super/usr/portage/distfiles/ ftp://baz.zuzino.mipt.ru/ http://baz.zuzino.mipt.ru/gentoo/odin/ ftp://ftp.citkit.ru/pub/Linux/gentoo/ http://distfiles.gentoo.org/" LANG="ru_RU.UTF-8" LINGUAS="ru de fr fi nl it es ja et" MAKEOPTS="-j3" PKGDIR="/usr/portage//packages/x86/" PORTAGE_TMPDIR="/var/tmp" PORTDIR="/usr/portage/" PORTDIR_OVERLAY="/usr/local/portage" SYNC="rsync://rsync.gentoo.org/gentoo-portage" USE="16bit 3ds 7zip X X509 a52 aac aalib abook accounting acl acpi activefilter ada adabas adns adsl afs aim aimextras aio allegro alsa amarok amd amr amuled ansi ao aotuv apache2 applet araneida ares arts artswrappersuid artworkextra aserve asf asm asterisk async atlas atm auctex audacious audiofile auth automount avahi avalon avantgo ax25 bash-completion bcmath bcp bdf beep berkdb bgpclassless bidi big-tables bigpatch bind-mysql birdstep bjam bl blas blender-game bluetooth bmp bonjour bonobo bookmarks bri browserplugin buffysize bzip2 c++ c3p0 cairo calendar canna cap capi caps cardbus cdb cdda cddb cdf cdinstall cdio cdparanoia cdr cdrom cegui cg cgi chasen checkpath chipcard chm chroot cis cjk ck-plus clamav clamd clanJavaScript clanVoice cle266 cli clisp cln corba cracklib crypt cscope css csv ctype cups curl curlwrappers cvsgraph daap db2 dba dbase dbcp dbi dbm dbmaker dbus dbx dcc debugger devmap dga dhcp dict dio directfb discard-path disk-cache diskio djbfft djvu dlloader dlopen dlz dnd dnsdb doc double-precision dpms drac dri dsml dssi dtaus dts dv dvb dvd dvdr dvdread dvi dxr3 dynagraph dynamic eap-tls eb ecc edl effects elf emboss emoticon empress encode enscript esd esoob esx ethereal examples exif expat extensions extraengine extras fam fame fastcgi fat fbcon fbdev fbsplash festival ffcall ffmpeg fftw figlet filepro firebird firefox fits flac flash flatfile flood fltk fluidsynth fmod fortran fping fpx frascend freetds freetts freewnn frontbase ftp fuse fwdzone gatos gb gcj gcl gdal gdbm geometry geos ggi gif gimp ginac glep glgd glitz glut glx gmail gmailtimestamps gmp gmtfull gmthigh gmtsuppl gmttria gnokii gnome gnome-print gnomecanvas gnomedb gnuplot gnutls gpgme gphoto2 gpm gps grammar graphicsmagick graphviz grass gs gsl gsm gsnd gssapi gstreamer gtalk gtk gtk2 gtkhtml guile gzip h323 hal hardened haskell hbci hddtemp hdf hdf5 hfs hlapi hostap howl howl-compat html http httpd hyperwave-api ibam ical icc icecast icon iconv icp icq icu id3 ide idea idl idled idn ieee1394 ifc iksemel image imagemagick imap imlib imlib2 informix ingres inifile inkjar inline innodb intl iodbc ipod ipppd iproute2 ipv6 irc irda isdn isdnlog itcl j2ee jabber jack jack-tmpfs jai java java-external javacomm javamail javascript jbig jboss jce jcs jfs jikes jimi jit jms jmx john jp2 jpeg jpeg2k jpty jta jumpplay junit jython kcal kde kdepim kerberos kexi key-screen keyscrub kig-scripting kipi ladcca ladspa lame lapack latex lcms ldap leim libabcl libcaca libclamav libdsk libedit libg++ libgda libsamplerate libtommath libvisual libwww lighttpd lirc live lj lm_sensors log4j logitech-mouse logrotate logwatch ltsp lua lzo lzw mad madwifi mail mailbox maildir maildrop mailwrapper math matroska maya-shaderlibrary mbox mbrola mbx mcal mccp mcve md5sum mdb memcache messages metar mew mhash mikmod mime mimencode ming mixer mjpeg mmap mmx mmxext mng mnogosearch mod mod_irc mod_lisp mod_muc mod_pubsub mod_python mode-force mode-owner mode-paranoid modperl modplug moneyplex mono mopac7 mounts-check mouse mozcalendar mozdevelop moznocompose moznoirc moznomail mozxmlterm mp3 mp4live mpd-mad mpeg mpeg2 mplayer mppe-mppc mpqc mschap msdav msession mslu msn msnextras msql mssql mudflap muine mule musepack musicbrainz mysql mysqli mythtv mzscheme nagios-dns nagios-game nagios-ntp nagios-ping nagios-ssh nas nautilus ncurses neXt network nfs nls nntp nptl nsplugin nspr ntfs ntlm numarray numeric nvidia nvram oav objc objc-gc ocaml octave odbc ode ofx ogdi ogg ogre openal openbabel openexr opengl openssh openssl oracle ortp osc pam pango patented pcmcia pcntl pcre pda pdf pdfkit pdflib pear pear-db perl pfpro pg-hier pg-intdatetime pg-vacuumdelay php pic pike player plib plotutils plugin plx pmu png pnp pop portaudio posix postgres povray ppds pppd pymol pyste python qdbm qemu-fast qhull qt quicktime quotas quotes radius rar razor rc5 rcu rdesktop readline real realms recode reiser4 reiserfs rhino rpc rrdtool rss rtc ruby samba sapdb sasl sbcl sblive scanner scp screen script scsh sdk sdl search search-screen semanticfix sensord servlet-2.3 servlet-2.4 session sftp sftplogging sguil sharedext sharedmem shorten shout silc simplexml skey slang slp smartcard smarty smime smp sms smtp sndfile snmp soap sockets socks5 soundtouch source sourcecaps sox spamassassin speech speedo speex spell spf spl spreadsheet sql sqlite sqlite3 srp srs srv sse sse-filters sse2 ssl startup-notification staticsocket stream streamzap struts subject-rewrite subp subtitles subversion svg svgz swarmcache swat sybase sybase-ct sylpheed sysfs syslog sysvipc szip t1lib tcltk tcpd tdb tetex text tga theora thesaurus threads thumbnail tidy tiff timidity tokenizer tomsfastmath tools tos transcode translator truetype truetype-fonts type1 type1-fonts ucs2 ucs4 udev uml unicode ups urandom usb userlocales utf8 uudeview v4l v4l2 vcd vcdimager videos vidix vim vim-pager visualization vlm vorbis wddx web webdav webservices wifi win32codecs withsamplescripts wma wma123 wmf wordperfect wv wxwindows x264 x86 xanim xattr xface xfs xine xinetd xmail xml xml2 xmldoclet xmlreader xmlrpc xosd xpm xrandr xscreensaver xsl xslt xv xvid xvmc yahoo yaz yiff yv12 zeo zero-penalty-hit zeroconf zip zlib elibc_glibc kernel_linux linguas_ru linguas_de linguas_fr linguas_fi linguas_nl linguas_it linguas_es linguas_ja linguas_et userland_GNU" Unset: ASFLAGS, CTARGET, LC_ALL, LDFLAGS
Could you please try the current stable coq-8.0_p3. It seems to work fine for me! Thanks, Markus
It's a bit old, but it could be that you updated ocaml without reemerging all the needed libraries (like lablgtk in this case). Please try to do so and report here if it still fails.
@sci folks - math-proof is not a valid bugzilla alias; please either create one or change metadata.xml to point to something else. Thanks.
I am closing this bug since the original poster hasn't responded for a long time and the more recent coq-8.0_p3 is stable on all arches. Please re-open should this issues still be a problem.
