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 -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]
