Bug#353493: marked as done (coq: Cannot compile CoRN; infinite memory-eating loop in "intuition" execution in power_k_n.)
Your message dated Sun, 19 Feb 2006 04:32:08 -0800
with message-id <E1FAnjU-0000PK-7M@spohr.debian.org>
and subject line Bug#353493: fixed in coq 8.0pl3-2
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)
--- Begin Message ---
Package: coq
Version: 8.0pl3-1
Severity: normal
Something weird must have happened in the compilation of Coq on i386,
or a Debian patch wreaks havoc. The coq in /usr/bin/coq cannot compile
the CoRN library, but a self-compiled CoRN (with the stock Debian
OCaml) from upstream tarball + OCaml 3.09.1 adaptation patch can.
Exact symptoms: when trying to compile the power_k_n lemma in
algebra/CMonoids.v, it just enters a busy loop (100% CPU), consuming
ever more memory until it runs out of addressing space (hits the 4GB
barrier), while evaluating an "intuition".
To reproduce:
- unpack attached tarball
- cd CoRN
- export COQTOP=/usr/
- make algebra/CMonoids.vo
-- System Information:
Debian Release: testing/unstable
APT prefers unstable
APT policy: (500, 'unstable'), (1, 'experimental')
Architecture: i386 (x86_64)
Shell: /bin/sh linked to /bin/bash
Kernel: Linux 2.6.15-deb1-64bit
Locale: LANG=fr_LU.UTF-8, LC_CTYPE=fr_LU.UTF-8 (charmap=UTF-8)
Versions of packages coq depends on:
ii coq-libs 8.0pl3-1 proof assistant for higher-order l
ii libc6 2.3.5-13 GNU C Library: Shared libraries an
ii libncurses5 5.5-1 Shared libraries for terminal hand
Versions of packages coq recommends:
ii coqide 8.0pl3-1 proof assistant for higher-order l
ii proofgeneral-coq 3.5-3 ProofGeneral support for coq
-- no debconf information
--- End Message ---
--- Begin Message ---
Source: coq
Source-Version: 8.0pl3-2
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.0pl3-2_all.deb
to pool/main/c/coq/coq-libs_8.0pl3-2_all.deb
coq7-libs_8.0pl3-2_all.deb
to pool/main/c/coq/coq7-libs_8.0pl3-2_all.deb
coq_8.0pl3-2.diff.gz
to pool/main/c/coq/coq_8.0pl3-2.diff.gz
coq_8.0pl3-2.dsc
to pool/main/c/coq/coq_8.0pl3-2.dsc
coq_8.0pl3-2_i386.deb
to pool/main/c/coq/coq_8.0pl3-2_i386.deb
coqide_8.0pl3-2_i386.deb
to pool/main/c/coq/coqide_8.0pl3-2_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 353493@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: Sun, 19 Feb 2006 11:33:21 +0000
Source: coq
Binary: coq7-libs coqide coq-libs coq
Architecture: source all i386
Version: 8.0pl3-2
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: 353493
Changes:
coq (8.0pl3-2) unstable; urgency=low
.
* Added coq-8.0pl3-ocaml-3.09.dpatch in order to prevent intuition from
looping forever, closes: #353493.
Files:
548a296b46bb18c10acb0175a6a50396 891 math optional coq_8.0pl3-2.dsc
c871e14e4f6a3e861ea351fa8e0d6da2 16289 math optional coq_8.0pl3-2.diff.gz
9a0fdcb82fd28c013f9aebc0e9dc79ad 3737024 math optional coq-libs_8.0pl3-2_all.deb
953b60e6a96afebda37ffddcfdcb2e5b 3812424 math optional coq7-libs_8.0pl3-2_all.deb
a09ea7f959b72228c91cd2520a7fd3a8 6111850 math optional coq_8.0pl3-2_i386.deb
7a2d32ee778f56c00bac079cadcdf79a 3441578 math optional coqide_8.0pl3-2_i386.deb
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.2 (GNU/Linux)
iD8DBQFD+GLBIae1O4AJae8RAr88AJoDTtRc9CLVawTpxLNICdMSxHMKKACfSuiW
WTRAVCoVevUxYXMTZgSiMw0=
=RtmT
-----END PGP SIGNATURE-----
--- End Message ---
Reply to: