The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 19/08/2016 19:08, Ralf Jung wrote:

> On 19.08.2016 18:37, Jonathan Leivent wrote:
>> For coqchk the issue is that it checks module "inclusion", not actual
>> definition usage.  Hence it will report that axioms are "present' when
>> Print Assumptions (even without plugin misbehavior) does not.  But, it
>> doesn't load plugins, hence is safe from "plugin misbehavior".
> 
> Is this actually true? Sure coqchk does not load plugins, but that still
> leaves the question open of what coqchk is actually checking. As far as
> I understand, it checks the .vo files, so if a plugin manages to make
> "good" .vo files from "bad" .v files, coqchk would not catch that.  For
> example, the plugin could alter the statement that has been proven such
> that the .vo file contains a valid proof of *some* statement (but not
> the one the user wants), and the .v files contains an *invalid* proof
> (messed with by the plugin) of the statement the user wants.

You are right.

What you can do is to write a new .v file containing only the statements
of the theorems you are interested in (and the definitions necessary to
state them). The proofs will be trivial, just apply the theorems you
proved using plugins beforehand. [1] Then erase all the plugins from
your system and run coqc on your new file. You will get a bunch of
warning messages about missing plugins, but no actual failures. Finally
you can run coqchk on that .vo file. That way, you only have to trust
the basic parser of coqc and the checker of coqchk.

Best regards,

Guillaume

[1] For instance, the whole Feit-Thompson development was compressed
into a 200-line Coq file that expresses everything, from a definition of
natural numbers to the odd-order statement. (The part about erasing all
the plugins from the system would not apply though, since SSReflect
syntax was used for this file.)