The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

----- Mail original -----
> Hi,
> 
> Similar to Duckki Oe [1] I would like to get a listing of all
> lemmas and definitions that are not used in a certain Coq
> development. Similar to [2], I guess that this is relatively easy
> to achieve with a plugin.
> 
> If I were to write such a plugin, were should I start searching
> for all declarations known to the system? I guess a vernacular
> has access to the current module, from where I could search
> dependent modules with all declarations therein. Where do I find
> this current module?
> 

This remains me of the recursive traversal done by "Recursive Extraction".
You could have a look at toplevel_env and related functions in
plugins/extraction/extract_env.ml. Another source of inspiration could
be the "Print Assumption" command (see library/assumptions.ml).

If you restrict to standard developments (no advanced modules or functors),
such a dead-code analyze is rather easy indeed, while a more complete tool
could be rather tricky...

Best,
Pierre


> 
> [1] https://sympa.inria.fr/sympa/arc/coq-club/2013-06/msg00141.html
> [2] https://sympa.inria.fr/sympa/arc/coq-club/2012-04/msg00078.html
>