The Coq mailing list

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

Hi,

On 19.08.2016 14:58, Pierre Courtieu wrote:
> Isn't it just that we need an option coqchk --list-dependencies-of
> Foo. Where Foo is a lemma?
> 
> In other words we need the equivalent of Print Assumption Foo in coqchk.

I think that would be pretty hard to use. I don't want *any* of the
lemmas in our development to use axioms, but I won't list 1k lemma names
when calling coqchk... sure there will be theorems exercising "the most
important bits of the entire development", but having something actually
check the entire development would ensure that we don't miss to "Print
Assumptions" on the one helper lemma we forgot about that's not used
anywhere here (but maybe *is* used in some reverse dependencies and/or
in on-paper reasoning).

However, if "--list-dependencies-of" would take wildcards, like "iris.*"
that could work.. oh wait, no. That would also cover all the reexported
unused axioms from the standard library, right?

Kind regards,
Ralf