Bug#585452: marked as done (coq: FTBFS with OCaml 3.12 because of bugfix in typechecking of inheritance)
Your message dated Fri, 02 Jul 2010 15:20:18 +0000
with message-id <E1OUi2M-0003cQ-HE@ries.debian.org>
and subject line Bug#585452: fixed in coq 8.2.pl2+dfsg-1
has caused the Debian Bug report #585452,
regarding coq: FTBFS with OCaml 3.12 because of bugfix in typechecking of inheritance
to be marked as done.
This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.
(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)
--
585452: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=585452
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message ---
- To: Debian Bug Tracking System <submit@bugs.debian.org>
- Subject: coq: FTBFS with OCaml 3.12 because of bugfix in typechecking of inheritance
- From: Stéphane Glondu <glondu@debian.org>
- Date: Thu, 10 Jun 2010 18:47:17 +0200
- Message-id: <4C111715.8000900@debian.org>
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
--- End Message ---
--- Begin Message ---
Source: coq
Source-Version: 8.2.pl2+dfsg-1
We believe that the bug you reported is fixed in the latest version of
coq, which is due to be installed in the Debian FTP archive:
coq-theories_8.2.pl2+dfsg-1_all.deb
to main/c/coq/coq-theories_8.2.pl2+dfsg-1_all.deb
coq_8.2.pl2+dfsg-1.debian.tar.gz
to main/c/coq/coq_8.2.pl2+dfsg-1.debian.tar.gz
coq_8.2.pl2+dfsg-1.dsc
to main/c/coq/coq_8.2.pl2+dfsg-1.dsc
coq_8.2.pl2+dfsg-1_amd64.deb
to main/c/coq/coq_8.2.pl2+dfsg-1_amd64.deb
coq_8.2.pl2+dfsg.orig.tar.gz
to main/c/coq/coq_8.2.pl2+dfsg.orig.tar.gz
coqide_8.2.pl2+dfsg-1_amd64.deb
to main/c/coq/coqide_8.2.pl2+dfsg-1_amd64.deb
libcoq-ocaml-dev_8.2.pl2+dfsg-1_amd64.deb
to main/c/coq/libcoq-ocaml-dev_8.2.pl2+dfsg-1_amd64.deb
A summary of the changes between this version and the previous one is
attached.
Thank you for reporting the bug, which will now be closed. If you
have further comments please address them to 585452@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Stéphane Glondu <glondu@debian.org> (supplier of updated coq package)
(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@debian.org)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512
Format: 1.8
Date: Fri, 02 Jul 2010 15:25:15 +0200
Source: coq
Binary: coq coqide coq-theories libcoq-ocaml-dev
Architecture: source amd64 all
Version: 8.2.pl2+dfsg-1
Distribution: unstable
Urgency: low
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Stéphane Glondu <glondu@debian.org>
Description:
coq - proof assistant for higher-order logic (toplevel and compiler)
coq-theories - proof assistant for higher-order logic (theories)
coqide - proof assistant for higher-order logic (gtk interface)
libcoq-ocaml-dev - development libraries and tools for Coq
Closes: 585452
Changes:
coq (8.2.pl2+dfsg-1) unstable; urgency=low
.
* New upstream release
- compiles with OCaml 3.12 (Closes: #585452)
- remove 0001-Update-for-why-2.19.patch (applied upstream)
- add 0002-Remove-dependency-to-Unix-from-module-Profile.patch
* Use dh with overrides
* debian/control:
- remove Stefano and Remi from Uploaders
- replace Conflicts with Breaks
- bump Standards-Version to 3.9.0
* Switch source package format to 3.0 (quilt)
Checksums-Sha1:
93ceac9f6389f1fb924a21b038419ed34e1f1fe7 2157 coq_8.2.pl2+dfsg-1.dsc
e994ae8621cfb61f221312252fe0f6d2f5b57784 3142575 coq_8.2.pl2+dfsg.orig.tar.gz
f0982c65e58ad3c6dd658405649dc93d478b7c87 16779 coq_8.2.pl2+dfsg-1.debian.tar.gz
fb335562adda3353fbf5c54675c7a85f3d345a21 15354950 coq_8.2.pl2+dfsg-1_amd64.deb
cf45364f615d1dee357c8242e66788bb0a714b48 6553352 coqide_8.2.pl2+dfsg-1_amd64.deb
fb74fe8bd2739ead9189b9b7d77ac20de86ddd75 18387420 coq-theories_8.2.pl2+dfsg-1_all.deb
3e9de30c5e61229377c669741065439fa2a862af 6085774 libcoq-ocaml-dev_8.2.pl2+dfsg-1_amd64.deb
Checksums-Sha256:
5d760efdb2dc5c08220a3f4140fba30d446ef58322f5923b001313a76909150b 2157 coq_8.2.pl2+dfsg-1.dsc
a731c1313a3a124f95d8b54842553b9bef6ef30beaf19de2afc2a11429d14780 3142575 coq_8.2.pl2+dfsg.orig.tar.gz
817965fc8e0cffd51495c266dbaecf0d34eb826f64bca420c4825d08e8f329c6 16779 coq_8.2.pl2+dfsg-1.debian.tar.gz
113112bac64002428b44096e90af97627b4c7fff0a80c7a2536edfb3e179747f 15354950 coq_8.2.pl2+dfsg-1_amd64.deb
f955ee847c7c030091ed7bb881f77de08c06002be03ad4f7a8a7f5d7041b25c6 6553352 coqide_8.2.pl2+dfsg-1_amd64.deb
54c3cd8f6eb66c98a6e157b33b957182a61767a19b1d6b37d4945029a26e8a40 18387420 coq-theories_8.2.pl2+dfsg-1_all.deb
fc5fbfb86e8d078774838ed040bbef85b07eb8ce55d1585ef43b41eaf7ad5574 6085774 libcoq-ocaml-dev_8.2.pl2+dfsg-1_amd64.deb
Files:
3a026518c5d8b4adf35b79cad23629f2 2157 math optional coq_8.2.pl2+dfsg-1.dsc
64093f3b22d6f49418b4d5267925141b 3142575 math optional coq_8.2.pl2+dfsg.orig.tar.gz
22f7bc31e1ad9289856fb92824e0e2bf 16779 math optional coq_8.2.pl2+dfsg-1.debian.tar.gz
140feb97b61e674b94a3ae4474e537b0 15354950 math optional coq_8.2.pl2+dfsg-1_amd64.deb
86a438a76340348dc56bae2df09ab1f7 6553352 math optional coqide_8.2.pl2+dfsg-1_amd64.deb
6d5a0460aa6cea104e3e86c5eae7e5a3 18387420 math optional coq-theories_8.2.pl2+dfsg-1_all.deb
79c302d333abf29eb8e7027945c426c6 6085774 ocaml optional libcoq-ocaml-dev_8.2.pl2+dfsg-1_amd64.deb
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
iQIcBAEBCgAGBQJMLff5AAoJEHhT2k1JiBrTV5QQAKsghiJlXJkzjVrAKma/iu8Q
i783IB/P4IClgwbvTh/2F93jqLCfFJ5SZ9UC4rZ+bh/c0quIcDHaighUwWdkCmqg
dsWqcWVjJM6e1wnX8j2f4jwb4tdNqaBpX2bs+OEdYRpv+4/n3+fzhNEDUm4UMp1z
BBO0puFJSkUpLfcnGV6iDh0kUaaxaKeZsf+VtOCsjG/nmAkQTRAChpwiN9XgztNy
fI6fVg8Qa0Uj3xJJ18i7DcJwevQeRC98jgEQxGOWSyCrYL1VhaVqi5RINqPOHpKG
pdKWE2A24bQitWlV1gCu2CJVzD8BU50zVg9mSP7qDeCIbKOT1PLrs+D4KDWYjERc
1F39DpLba1sBqy36qdS3M3PEREaaOTEJcXqfmMQoOrwXLTDb6VlBDg/1OWZCGbTE
WJbHoZdq1yQqUrjVphoGU29YPILTvwQfTaKjhYJceAOzko3VHzRb9xaaoYM/WBCd
SCtrxAuObwhy9xM10+1U3KonrgzlBfnura4RTvkzHf2KWycYUqK+98Bvkezdx78x
YQsDZgALnCuOaADBHLb88go2pgvHL6G3tY/HKS5KtTp9p1NrbSgUKH5WaWd4yjqX
Sgo/OzRHq2FQ/4cu8Hs3eg2OQJJh/NmhDUc8j6Gca2XjGUjHLOGJKWLbveYfn1tT
rJbhILhPOroADRVfA5/i
=zyT3
-----END PGP SIGNATURE-----
--- End Message ---
Reply to: