Bug#340185: marked as done (coq: FTBFS: implementation doesn't match interface: parsing/pcoq*)
Your message dated Mon, 21 Nov 2005 13:48:16 -0800
with message-id <E1EeJWK-0001F7-6A@spohr.debian.org>
and subject line Bug#340185: fixed in coq 8.0pl2-4
has caused the attached Bug report 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 I am
talking about this indicates a serious mail system misconfiguration
somewhere. Please contact me immediately.)
Debian bug tracking system administrator
(administrator, Debian Bugs database)
--------------------------------------
Received: (at submit) by bugs.debian.org; 21 Nov 2005 18:00:30 +0000
>From stigge@antcom.de Mon Nov 21 10:00:30 2005
Return-path: <stigge@antcom.de>
Received: from mail-out.m-online.net ([212.18.0.9])
by spohr.debian.org with esmtp (Exim 4.50)
id 1EeFxu-0001Ix-8k
for submit@bugs.debian.org; Mon, 21 Nov 2005 10:00:30 -0800
Received: from mail.m-online.net (svr20.m-online.net [192.168.3.148])
by mail-out.m-online.net (Postfix) with ESMTP id 25ECB7004A;
Mon, 21 Nov 2005 18:58:38 +0100 (CET)
Received: from atari.stigge.org (ppp-82-135-1-135.mnet-online.de [82.135.1.135])
by mail.m-online.net (Postfix) with ESMTP id 49EFB136C6F;
Mon, 21 Nov 2005 19:00:24 +0100 (CET)
Received: from [192.168.5.99] (localhost [127.0.0.1])
by atari.stigge.org (Postfix) with ESMTP id 0493C1033FA7C;
Mon, 21 Nov 2005 19:00:32 +0100 (CET)
From: Roland Stigge <stigge@antcom.de>
To: submit@bugs.debian.org
Subject: coq: FTBFS: implementation doesn't match interface: parsing/pcoq*
Message-Id: <[🔎] 20051121180032.0493C1033FA7C@atari.stigge.org>
Date: Mon, 21 Nov 2005 19:00:32 +0100 (CET)
Delivered-To: submit@bugs.debian.org
X-Spam-Checker-Version: SpamAssassin 2.60-bugs.debian.org_2005_01_02
(1.212-2003-09-23-exp) on spohr.debian.org
X-Spam-Level:
X-Spam-Status: No, hits=-7.5 required=4.0 tests=BAYES_00,HAS_PACKAGE,
RCVD_IN_SORBS autolearn=no version=2.60-bugs.debian.org_2005_01_02
Package: coq
Version: 8.0pl2-3
Severity: serious
Hi,
building the package coq in a clean sid build environment
(with pbuilder) on i386 results in:
=========================================================================
[...]
OCAMLC interp/coqlib.mli
OCAMLC interp/coqlib.ml
OCAMLC library/declare.mli
OCAMLC library/declare.ml
OCAMLC -a -o interp/interp.cma
OCAMLC parsing/coqast.ml
OCAMLC parsing/ast.mli
OCAMLC parsing/ast.ml
OCAMLC parsing/termast.mli
OCAMLC parsing/termast.ml
OCAMLC parsing/extend.mli
OCAMLC parsing/extend.ml
OCAMLC parsing/esyntax.mli
OCAMLC parsing/esyntax.ml
OCAMLC -rectypes proofs/tacexpr.ml
OCAMLC toplevel/vernacexpr.ml
OCAMLC parsing/pcoq.mli
OCAMLC4 parsing/pcoq.ml4
Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead.
File "parsing/pcoq.ml4", line 620, characters 4-18:
Warning Y: unused variable l'.
The implementation parsing/pcoq.ml4
does not match the interface parsing/pcoq.cmi:
Values do not match:
val main_entry : ((Coqast.t -> Util.loc) * '_a) option Gram.Entry.e
is not included in
val main_entry : (Util.loc * Vernacexpr.vernac_expr) option Gram.Entry.e
make[1]: *** [parsing/pcoq.cmo] Error 2
make[1]: Leaving directory `/tmp/buildd/coq-8.0pl2'
make: *** [build-stamp] Error 2
=========================================================================
Thanks for considering.
--
DARTS - Debian Archive Regression Test Suite
http://darts.alioth.debian.org/
---------------------------------------
Received: (at 340185-close) by bugs.debian.org; 21 Nov 2005 21:57:21 +0000
>From katie@ftp-master.debian.org Mon Nov 21 13:57:21 2005
Return-path: <katie@ftp-master.debian.org>
Received: from katie by spohr.debian.org with local (Exim 4.50)
id 1EeJWK-0001F7-6A; Mon, 21 Nov 2005 13:48:16 -0800
From: Samuel Mimram <smimram@debian.org>
To: 340185-close@bugs.debian.org
X-Katie: $Revision: 1.56 $
Subject: Bug#340185: fixed in coq 8.0pl2-4
Message-Id: <E1EeJWK-0001F7-6A@spohr.debian.org>
Sender: Archive Administrator <katie@ftp-master.debian.org>
Date: Mon, 21 Nov 2005 13:48:16 -0800
X-Spam-Checker-Version: SpamAssassin 2.60-bugs.debian.org_2005_01_02
(1.212-2003-09-23-exp) on spohr.debian.org
X-Spam-Level:
X-Spam-Status: No, hits=-6.0 required=4.0 tests=BAYES_00,HAS_BUG_NUMBER
autolearn=no version=2.60-bugs.debian.org_2005_01_02
Source: coq
Source-Version: 8.0pl2-4
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-libs_8.0pl2-4_all.deb
to pool/main/c/coq/coq-libs_8.0pl2-4_all.deb
coq7-libs_8.0pl2-4_all.deb
to pool/main/c/coq/coq7-libs_8.0pl2-4_all.deb
coq_8.0pl2-4.diff.gz
to pool/main/c/coq/coq_8.0pl2-4.diff.gz
coq_8.0pl2-4.dsc
to pool/main/c/coq/coq_8.0pl2-4.dsc
coq_8.0pl2-4_i386.deb
to pool/main/c/coq/coq_8.0pl2-4_i386.deb
coqide_8.0pl2-4_i386.deb
to pool/main/c/coq/coqide_8.0pl2-4_i386.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 340185@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Samuel Mimram <smimram@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: SHA1
Format: 1.7
Date: Mon, 21 Nov 2005 19:52:53 +0100
Source: coq
Binary: coq7-libs coqide coq-libs coq
Architecture: source all i386
Version: 8.0pl2-4
Distribution: unstable
Urgency: low
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Samuel Mimram <smimram@debian.org>
Description:
coq - proof assistant for higher-order logic (toplevel and compiler)
coq-libs - proof assistant for higher-order logic (theories)
coq7-libs - proof assistant for higher-order logic (Coq 7 theories)
coqide - proof assistant for higher-order logic (gtk interface)
Closes: 340185
Changes:
coq (8.0pl2-4) unstable; urgency=low
.
* Added ocaml309.dpatch patch to compile cleanly with OCaml 3.09,
closes: #340185.
* Removed recommends on coq-doc which is not in main anymore.
* Updated standards version to 3.6.2, no changes needed.
Files:
46c3f97cff31d2d0c001611ed06973b3 882 math optional coq_8.0pl2-4.dsc
a7dcfd2964389244aa641320a886f260 12018 math optional coq_8.0pl2-4.diff.gz
2c31ea8067d38b584e08a2e8e3907a08 3735548 math optional coq-libs_8.0pl2-4_all.deb
71c1b229dd59c263b41a5ca20c1a3341 3811086 math optional coq7-libs_8.0pl2-4_all.deb
71444c7183660bdd9b310b019a5141f9 6089540 math optional coq_8.0pl2-4_i386.deb
7dd0c5fa4a7beb31804f04137e1cf231 4140764 math optional coqide_8.0pl2-4_i386.deb
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.2 (GNU/Linux)
iD8DBQFDgiPbIae1O4AJae8RAiC4AJ9wNpqY4jLL9NurtRyvxxMc0lDqdgCdFKr7
PRn5rDsyzvEH5tbrOo7YPzA=
=fMTJ
-----END PGP SIGNATURE-----
Reply to: