The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi

Detecting reliably the end of a command is indeed difficult without calling Coq. Currently using emacs/proofgeneral is probably ok 99,9% of the time, but relying on coqc -time is safer imho.

If you want to do it by yourself by splitting, you have to keep the two following points in mind:

1) The script structuring characters need a special treatment: "+" "*", "-" "{" and "}". You need some context to know if an occurrence of them is a command or a part of an _expression_. In proofgeneral I check if previous non whitespace char is itself an end of command, if yes then the char is also an end of command. This is recursive of course because of ". }}}". Notice that ".}" or ".+" are not accepted by coq.

2) And of course Coq accepts nested comments so you need to detect them too.

If you do that then you are as good as emacs/proofgeneral (and probably faster).

Hope this helps,
Pierre

2013/4/19 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