[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#585452: coq: FTBFS with OCaml 3.12 because of bugfix in typechecking of inheritance

Package: src:coq
Version: 8.2.pl1+dfsg-6
Severity: normal
User: debian-ocaml-maint@lists.debian.org
Usertags: ocaml312-ftbfs

Hello,

While rebuilding all packages with a SVN snapshot of OCaml (version
3.12.0+dev26, revision 10544), your package failed to build on amd64.

Revelant part:

"ocamlc" -rectypes  -g -thread -I +lablgtk2 -I config -I tools -I tools/coqdoc -I scripts -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I contrib/omega -I contrib/romega -I contrib/micromega -I contrib/ring -I contrib/dp -I contrib/setoid_ring -I contrib/xml -I contrib/extraction -I contrib/interface -I contrib/fourier -I contrib/cc -I contrib/funind -I contrib/firstorder -I contrib/field -I contrib/subtac -I contrib/rtauto  -I "+camlp5"   -c ide/undo.ml
File "ide/undo.ml", line 1, characters 0-1:
Error: The implementation ide/undo.ml
       does not match the interface ide/undo.cmi:
       Class declarations do not match:
         class undoable_view :
           ([> Gtk.text_view ] as 'a) Gtk.obj ->
           object
             val history : action Stack.t
             val nredo : action Stack.t
             val obj : 'a Gtk.obj
             val redo : action Queue.t
             method accepts_tab : bool
             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_accepts_tab : bool -> 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 accepts_tab : bool
             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_accepts_tab : bool -> 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 ] as 'b) Gtk.obj = 'b Gobject.obj
       Type 'a = [> `container | `gtk | `textview | `widget ]
       is not compatible with type
         'b = [> `container | `gtk | `textview | `widget ]
make[2]: *** [ide/undo.cmo] Error 2
make[2]: Leaving directory `/tmp/coq-8.2.pl1+dfsg'
make[1]: *** [check] Error 2
make[1]: Leaving directory `/tmp/coq-8.2.pl1+dfsg'


The full build log is available at:

http://ocaml.debian.net/debian/ocaml3120dev26r10544/failures/coq_8.2.pl1%2Bdfsg-6%2B3.12.0%2Bdev26%2B10544%2B1_amd64.build


Best regards,

--
Stéphane
Reply to: