Bug#353493: coq: Cannot compile CoRN; infinite memory-eating loop in "intuition" execution in power_k_n.
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
Reply to: