The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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

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