The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>]

On 08/19/2016 02:54 PM, Ralf Jung wrote:
> Hi,
>
> > > > My proposal here would be to only show axioms which are actually used by
> > > > a name exported by one of the modules passed to coqchk.
> > Names which are not exported are still available via qualified names
> > when importing the module, so this makes sense to include them in the
> > list (i.e., if you are allowed to import the module, then you get the
> > power to use these axioms).
> Well, in some sense this is a heuristic.  But the point is, it should be
> possible to get a clean "coqchk" output if you don't actually use any
> axioms.  An axiom which is not (transitively) used by any symbol
> exported by any of my module, I would consider "unused".  If a client
> uses that axiom through the fully qualified name within my library,
> well, I doubt this can happen accidentally -- and after all, this *does*
> show up when they run "coqchk".
>
> However, I just realized that IIRC, Coq makes little different between
>
>    Require Import foo
>
> and
>
>    Import Module foo.
>      (* Paste file contents of foo.v here *)
>    End foo.
>
> This is problematic, as I would expect "coqchk" to report axioms used in
> symbols in the latter case (after all, the using happens within this
> module), but not in the former case.
>
> Maybe this really asks for library designers not to import axioms if
> they don't also use them.  But isn't it too late for that? For example,
> we import "Psatz" to get "lia", and this pulls in two dozens axioms
> about real numbers that we never want to use...
>
> Kind regards,
> Ralf

I think the point of the list of axioms returned by coqchk is just to 
give you the list of things you can access when importing the module. 
Making its behavior depend on namespacing considerations would be rather 
strange.

But yes, I think there is a need for omething like "Print Assumptions" 
in coqchk. But that should be theoremwise (meaning you ask the question 
for each theorem, or set of theorems).