The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Certainly, we would like to have some convenient method to determine 
that no unexpected axiom usage takes place in some part of a development.

Right now, we have Print Assumptions and coqchk.  However, neither quite 
does the desired job.  There are several reasons for this.

For Print Assumptions - this is currently just a per-definition check, 
hence it is difficult to use for a large development containing many 
definitions.  Furthermore, because it is run from the script itself, it 
is susceptible to "plugin misbehavior" - the ability of a plugin to 
alter the functionality of just about anything in a script, possibly 
causing Print Assumptions to misreport.

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

Some have suggested that coqchk, while remaining a module inclusion 
checker, could be used for the desired check provided that modules are 
careful about their inclusions.  The maximal care would be to completely 
segregate axiom-providing and axiom-consuming modules from others.  
There are two problems with this that I see.  One is that there are 
existing modules in the standard library and plugins that currently 
violate this rule. The other is that the rule itself may force module 
developers to contort their modularity in difficult ways just to 
accommodate this practice and create modularity problems in other areas.

I would rather not base axiom checking merely on inclusions, even if the 
standard library and plugins could be "cleaned up" in this regard.  I 
think the behavior of Print Assumptions is closer to what people 
actually want - but it needs to be made both wider in scope (something 
like allowing Print Assumptions on an entire module, which would check 
all definitions created in that module), and rendered somehow safe from 
"plugin misbehavior".  Do people agree with this?  If so, should this 
become part of coqchk, or be a separate tool?

-- Jonathan