The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I will probably build in support for [coqc -time] when I get a chance.  Currently, however, I don't care about splitting apart structured proof bullets; what I really want is a way to know "how much should I feed to coqtop before waiting for output, such that I don't hang, but such that I stop after every [Definition], [Hint], etc".  So I guess what I should do is use coqtop -emacs -time, and parse the output of that.

Currently, how I do this is by stripping comments, taking care to parse nested comments and comment-looking-things inside of strings correctly (because I don't need comments in the final output), looking for strings which have [. ] inside of them, and replacing that with [." ++ "] (which I'm not sure always works), and then splitting on a dot followed by whitespace.

Thanks,

Jason

On Mon, Apr 22, 2013 at 4:19 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

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