The Coq mailing list

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

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