coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: Enrico Tassi <enrico.tassi AT inria.fr>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Splitting a coq file into many parts
- Date: Fri, 19 Apr 2013 15:48:46 -0400
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:Hum, it seems you look for an hack, but I don't get what you want to
> (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.)
achieve...
Cheers
--
Enrico Tassi
- [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.