The Coq mailing list

[Duckki Oe <duckki AT mit.edu>]

Thanks for the replies. I realized my original question was too vague. Sorry 
about that.  Yes, because of hint databases, it's not easy to identify what's 
used or not used in proofs (a true dependency analysis). I could search the 
space by removing from hint DB one by one, but it will be slow even with 
automated tools, because my proofs take an hour to compile each time. I think 
we can identify positively what's used by turning all the lemmas in question 
into conjectures and printing assumptions. Then, we could possibly take the 
rest of definitions are not used. I was wondering if there is already a tool 
that can do this. 

-- Duckki



On Friday, June 21, 2013 at 5:12 PM, Jason Gross wrote:

> Oh, I see. I interpreted the original question to be "which lemmas are 
> neither used nor put into hint databases".
> 
> I think my scripts could be modified to first split apart "Hint" lines, so 
> that each hint line only adds one lemma to a database, and then tries, by 
> brute force, to see which hint lines can be removed without making the file 
> fail to compile. After that, it can do a syntactic check. This would be a 
> bit more work than the other version, though most of the infrastructure is 
> already in my scripts. 
> 
> -Jason
> 
> 
> On Fri, Jun 21, 2013 at 4:43 PM, Nuno Gaspar 
> <nmpgaspar AT gmail.com
>  
> (mailto:nmpgaspar AT gmail.com)>
>  wrote:
> > Hello.
> > 
> > Math Prover is right.
> > 
> > For instance, if you have
> > 
> > Lemma SomeLemmaX...
> > Lemma SomeLemmaY...
> > 
> > Hint Resolve SomeLemmaX SomeLemmaY.
> > 
> > Lemma SomeLemmaZ:
> > Proof.
> > auto.
> > Qed.
> > 
> > The question is: are both used, just one, or none?
> > 
> > I don't think you can answer that simply by syntactical analysis. 
> > 
> > 
> > Cheers.
> > 
> > 
> > 
> > 
> > 
> > 
> > 
> > 
> > 
> > 
> > 
> > 
> > 2013/6/21 Jason Gross 
> > <jasongross9 AT gmail.com
> >  
> > (mailto:jasongross9 AT gmail.com)>
> > > Math Prover: If lem_X is used as a hint by auto/crush, then it must 
> > > appear somewhere else in a "Hint" statement, except in the case that it 
> > > is declared as an Instance rather than as a Definition or Lemma (in 
> > > which case it is automatically added to the typeclass_instances 
> > > database).
> > > 
> > > I think the python scripts I wrote to minimize a buggy file (at 
> > > https://github.com/JasonGross/coq-bug-finder) can be used for this. In 
> > > particular, it shouldn't take me more than 0.5-2 hours to write a 
> > > script that will print out all of the definitions, lemmas, etc. of all 
> > > files included into a particular file which are not referenced after 
> > > some point. (Note that it only checks things by name, and so if you 
> > > have overlapping names, it might get confused. It's also recursive, in 
> > > that if you have Lemma A referencing 
> > > Lemma B, but Lemma A is unreferenced, then Lemma B also counts as 
> > > unreferenced, unless Lemma A appears after the cut-off point. If you 
> > > want, I can change this, too.) If you want me to, I can do this in the 
> > > next few days, or you can try it yourself (the relevant bit is 
> > > "try_remove_definitions" in find-bug.py). If you want me to do it, I'd 
> > > need a clearer idea of what you want to do, and possibly an example 
> > > repository (for example, it currently doesn't deal well with nested 
> > > directory structure). 
> > > 
> > > -Jason 
> > > 
> > > 
> > > On Fri, Jun 21, 2013 at 9:38 AM, Math Prover 
> > > <mathprover AT gmail.com
> > >  
> > > (mailto:mathprover AT gmail.com)>
> > >  wrote:
> > > > I think the problem here is
> > > > 
> > > > > "I put lemmas in hint databases"
> > > > 
> > > > Therefore, an emacs module that merely parses the *.v file won't
> > > > suffice, because it's possible that there is some Lemma lem_X, where:
> > > > 
> > > > *) the name lem_X does not appear anywhere else
> > > > *) however lem_X is used as as rewrite/resolve hint used by auto/crush
> > > > 
> > > > 
> > > > On Fri, Jun 21, 2013 at 6:35 AM, Kenneth Adam Miller
> > > > <kennethadammiller AT gmail.com
> > > >  
> > > > (mailto:kennethadammiller AT gmail.com)>
> > > >  wrote:
> > > > > You could write a definition for the coq language using Semantic in 
> > > > > Emacs
> > > > > 
> > > > > http://www.gnu.org/software/emacs/manual/html_node/emacs/Semantic.html
> > > > > 
> > > > > Semantic goes the extra mile in extensible and configurable editors 
> > > > > like
> > > > > Emacs by striving to rigorously understand the language and its 
> > > > > syntax. So
> > > > > if you wrote that, not only would you be helping the open source 
> > > > > community,
> > > > > but you would also provide yourself with a way to colorize all the
> > > > > un-referenced definitions/theorems in a module. And if you can 
> > > > > colorize
> > > > > them, you can put it into a configurable script!
> > > > > 
> > > > > 
> > > > > On Thu, Jun 20, 2013 at 3:00 PM, Duckki Oe 
> > > > > <duckki AT mit.edu
> > > > >  
> > > > > (mailto:duckki AT mit.edu)>
> > > > >  wrote:
> > > > > > 
> > > > > > Hi,
> > > > > > 
> > > > > > Is there a tool that can detect unreferenced definitions/theorems 
> > > > > > in a
> > > > > > module (or modules)? I'd like to clean up my modules and remove 
> > > > > > unnecessary
> > > > > > lemmas. But, I put lemmas in hint databases and it'll be very 
> > > > > > time consuming
> > > > > > to manually test if every single lemma is used. Thanks!
> > > > > > 
> > > > > > -- Duckki
> > 
> > 
> > 
> > -- 
> > Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 
> > dollars last year.
> > Marge: Bart! Don't make fun of grad students, they just made a terrible 
> > life choice. 
>