coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Splitting a coq file into many parts, Jason Gross, 04/11/2013
- Re: [Coq-Club] Splitting a coq file into many parts, Pierre Boutillier, 04/12/2013
- Re: [Coq-Club] Splitting a coq file into many parts, Enrico Tassi, 04/12/2013
- Re: [Coq-Club] Splitting a coq file into many parts, Enrico Tassi, 04/12/2013
- Re: [Coq-Club] Splitting a coq file into many parts, Jason Gross, 04/19/2013
- Re: [Coq-Club] Splitting a coq file into many parts, Pierre Courtieu, 04/22/2013
- Re: [Coq-Club] Splitting a coq file into many parts, Jason Gross, 04/22/2013
- Re: [Coq-Club] Splitting a coq file into many parts, Pierre Courtieu, 04/22/2013
- Re: [Coq-Club] Splitting a coq file into many parts, Jason Gross, 04/19/2013
- Re: [Coq-Club] Splitting a coq file into many parts, Pierre Boutillier, 04/12/2013
Archive powered by MHonArc 2.6.18.