Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Splitting a coq file into many parts

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Splitting a coq file into many parts


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Splitting a coq file into many parts
  • Date: Wed, 10 Apr 2013 18:26:01 -0400

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



Archive powered by MHonArc 2.6.18.

Top of Page