The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/30/2015 07:50 AM, Pierre-Marie Pédrot wrote:
> On 30/03/2015 13:48, Enrico Tassi wrote:
> > The code implementing the recursive traversal and looking for axioms
> > is in library/assumptions.ml, but I don't know if it can be reused as
> > such in the checker.
> Be aware that it is bugged, so that some care has to be taken.
>
> https://coq.inria.fr/bugs/show_bug.cgi?id=3948
>
> The bug seems to appear because of module trickery, and the checker acts
> notably differently from coqtop in this respect, so that it may go
> through just fine, but still. The checker is the checker!
>
> PMP

There are (at least?) two ways that can make a library inconsistent such 
that that coqc and coqtop wouldn't spot it - misbehaving plugins and 
misuse of axioms (most notably, using several axioms that together are 
inconsistent).  Correct?  Hence, since we are told to rely on coqchk to 
compensate for the first way, why not the second as well?

Adding such a feature to coqchk would supplement the previously 
discussed (on coqdev, at least) "assert assumptions" feature request, as 
that assert feature - although quite useful - would be susceptible to 
plugin misbehavior.

But, if bugs would be introduced into coqchk by doing this, then that 
rather brutally defeats the purpose.

-- Jonathan