The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Thanks, everyone.  coqc -time is a good start, though splitting on \.\s (that is, a dot followed by whitespace) seems to do approximately as well.

I have successfully used "coqtop -emacs" to split the file into definitions; the code is at https://github.com/JasonGross/coq-bug-finder/blob/master/split_definitions.py.  I welcome any better/faster ways to do this.  (As well as suggestions that I should comment particular lines, or my code in general, better.)

I want to figure out which lines are not necessary to compile a given line in a coq file; part of this involves attempting to remove definitions which define things which aren't used anywhere in the file.

-Jason

On Fri, Apr 12, 2013 at 5:04 AM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:

On Wed, Apr 10, 2013 at 06:26:01PM -0400, Jason Gross wrote:
> (I'm about to go source-dive CoqIDE and/or ProofGeneral, but I figured I'd
> ask here first to see if anyone could help me.)

Hum, it seems you look for an hack, but I don't get what you want to
achieve...

Cheers
--
Enrico Tassi