The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

[Warning: digression ahead.]

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.

It's not like I have any thoughts on how to remedy this, but I feel like
saying "malicious plugins can't harm you if you use coqchk" isn't
actually true. Admittedly, it is very unlikely for an accidental bug in
a plugin to trigger this.
  Or maybe this falls into the same category as "Definition False :=
True", though "don't Import/Export any modules / fully qualify
everything" doesn't help if the plugin is messing with the parser and
pretty-printer.

Kind regards,
Ralf