The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

On Mon, May 23, 2011 at 05:29:32PM +0200, Bruno Barras wrote:
> 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.
> 

i would dare conjecture a west european developer wouldn't be able
to fix this, do you have east comrades on staff?


> > 
> > 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).
>

i am not entirely sure the majority of your user base runs coqchk after
coqc passed and coqtop is happy :)

-- 
joro