Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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:
> (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




Archive powered by MHonArc 2.6.18.

Top of Page