The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 05/22/2011 04:36 PM, Georgi Guninski wrote:
> .vo that freezes coqchk (possibly forever).
> 
> attached are 2 .vo for Coq 8.3pl2.
> 
> j3a.vo was modified with vim so 2 [Definition] have the same name - this 
> results in a freeze in a coqchk (possibly forever).

Thanks. This one was a critical bug of coqchk. I've just commited a
patch (trunk and v8.3. v8.2 is imminent) to fix it.

> 
> j2.vo was produced with a patched version of Coq and unfortunately doesn't 
> pass coqchk, though coqtop is perfectly happy with it, especially with 
> Lemma aboutfalse (True and False keep their original meanings,the only 
> trick was disabling type checks, evidently coqtop does no type checks. 
> Lemma aboutfalse appears to be usable with vanilla coqc)
> 

Unlike coqchk, coqtop is not supposed to recheck .vo files it loads, so
as far as I understood your testcase, this is not a bug (as long as
coqchk rejects the forged .vo).

Bruno.