Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Combining multiple coq files into one

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Combining multiple coq files into one


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: AUGER Cédric <sedrikov AT gmail.com>
  • Cc: Sigurd Schneider <sigurd.schneider AT cs.uni-saarland.de>, coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Combining multiple coq files into one
  • Date: Thu, 9 May 2013 17:32:40 -0400

I don't currently use coqdep to get the dependencies, though I might do that in the future.  The problem that I'm trying to solve currently, though, is not figuring out the dependency chain (or a topological sort thereof), but inlining all of the code into a single file without running into name clashes.

-Jason


On Thu, May 9, 2013 at 3:19 PM, AUGER Cédric <sedrikov AT gmail.com> wrote:
Le Thu, 9 May 2013 14:17:41 -0400,
Jason Gross <jasongross9 AT gmail.com> a écrit :

> Hi,
> Thanks, but the intended output is a single stand-alone .v file,
> which I would then post-process.  I'm looking for a programmatic way
> to inline all of the non-stdlib dependencies of a .v file, as a first
> step in automatically minifying buggy code, to create a small test
> case.
>
> -Jason

Have you thought of using coqdep to get the dependencies? (I did not
really follow this thread, so maybe someone already talked of it.)




Archive powered by MHonArc 2.6.18.

Top of Page