The Coq mailing list

["Harley D. Eades III" <harley.eades AT gmail.com>]

Hi, everyone.

Great replies thus, far.

Would it not work to print the raw proof terms to a file and then
search those?  This would allow one to see exactly when a
particular lemma or definition is used.  It would of course take
sometime to generate the proof terms which would be quite large.

Cheers,
.\ Harley


On Jun 23, 2013, at 4:45 PM, Duckki Oe 
<duckki AT mit.edu>
 wrote:

> 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. 
>> 
> 
> 
>