The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If you go the route of turning things into conjectures and printing the assumptions, there's some python code in my repository (linked to previously) that will replace definitions/lemmas which aren't of the [Definition foo := bar.] type with [Definition foo : fooT.  Admitted.].

-Jason

On Sun, Jun 23, 2013 at 10:45 AM, 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.
>