The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi Jason,

Something that has been rewritten several times is how to split coq
files into sentences.
As soon :-) as the new coqdoc[1] will be merged with trunk, there will
be a command in the xml protocol (coqtop -ideslave) that takes a stream
and answers the position of the end of the first sentence in it.

For now, coqide heuristic is in ide/coq_lex.mll. It is : modulo
commentaries, string and spaces, a sentence is exactly one of '{', '}',
'-', '+', '*' or (anything that ends by a dot followed by a space (' ',
'\n', '\r', '\t', '\012') ).

The last implementation of it I know has been done by Enrico Tassi for
the time annotation machinery of the mathematical components library
[2]. I don't know where and in witch language the code is.

Your problem is much much more complicated. You want to split the file
in blocks where one proof is one block. Absolutely no one but coq knows
when coq will go in proof-mode. When I want to be able to isolate these
blocks for coqide highlighting mode (Hoping that maybe in 2017
gtksourceview will at last release the code folding feature), I end by
asking for any proof to start by the "Proof." sentence (and end by
"Qed." "Defined." or "Admitted.") !
If you are able to read a stack automaton written in xml, it is in
ide/coq.lang of the sources. (By the way, it is incomplete so please
tell me what is missing)

Thanks a lot for all the work you do for bug tacking even if coqdevs
reactivity is not fast, it helps a lot.

All the best,
Pierre B.

[1] https://github.com/thethirdman/coq
[2] http://ssr2.msr-inria.inria.fr/~jenkins/annotated/

On 11/04/2013 00:26, Jason Gross wrote:
> Hi,
> I would like to take a coq file, and split it apart into separate
> files (or strings of code), each of which is a single
> definition/lemma/notation/hint/etc.  For example, in a file with no
> sections and no local things, I would like to be able to split it
> apart into files a.v, b.v which has [Require Export a.], c.v which has
> [Require Export b.], etc, such that the last file is equivalent to the
> file I started with.  Equivalently, I would like a program which can
> take in a .v file, and split the file into a list of chunks [a, b, c,
> ...], so that if I had loaded the original file into CoqIDE, clicking
> the "evaluate next" button once would evaluate a, clicking it again
> would evaluate b, etc.
>
> Is there a good way to do this from bash, python, C, or some other
> language?
>
> (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.)
>
> Thanks,
> Jason