The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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

On May 9, 2013 4:26 AM, "Sigurd Schneider" <sigurd.schneider AT cs.uni-saarland.de> wrote:

Hi Jason,

please have a look at the attached file, I think it contains an example of what you have in mind. It works by omitting the "outer" modules and use the -R option to coqc instead. Emacs/proofgeneral supports this as well.

Sigurd

----- Original Message -----
From: "Jason Gross" <jasongross9 AT gmail.com>
To: "Gabriel Scherer" <gabriel.scherer AT gmail.com>
Cc: "coq-club" <coq-club AT inria.fr>
Sent: Thursday, May 9, 2013 9:49:20 AM
Subject: Re: [Coq-Club] Combining multiple coq files into one

Suppose you have directories A and B, and each has files A.v and B.v.
 Suppose B.A depends on A.A, and B.B depends on A.B, which depends on B.A.
 So the order must be A.A, B.A, A.B, B.B.  But if I do
Module A.
  Module A.
  End A.
End A.
Module B.
  Module  A.
  End A.
End B.
Module A.
  Module B.
  End B.
End A.
Module B.
  Module  B.
  End B.
End B.

I believe that Coq will complain on the second Module A that I already have
something named Module A.

-Jason


On Thu, May 9, 2013 at 3:15 AM, Gabriel Scherer
<gabriel.scherer AT gmail.com>wrote:

> I'm not sure I understand what the problem is. Do you have an example
> of a subdirectory + dependencies structure that makes the approach you
> have with "all files in the same directory" not work ? Intuitively it
> seems that a topological order of modules/files respecting the
> dependency relation should work in both case. Maybe the problem is
> that you first handle each subdirectory independently, then try to
> combine the result somehow, instead of handling them all at once as in
> the single-directory case?
>
> On Thu, May 9, 2013 at 7:58 AM, Jason Gross <jasongross9 AT gmail.com> wrote:
> > Hi,
> > Is there a way to consistently combine multiple coq files into a single
> coq
> > file, such that the output of coqing that file will be the same as if you
> > had coqed the original one?
> >
> > If the files are all in the same directory and don't have weird
> characters,
> > then I can wrap the contents of each file in [Module <filename>. ... End
> > <filename>.], and then shove them all in a single file so that there are
> no
> > forward references, and remove and [Require]s of that module, and replace
> > [Require Import] with [Import], and [Require Export] with [Export].
> > However, I have not figured out a good way to do this when files are in
> > subdirectories, and they depend on each other in such a way that I cannot
> > place all of the files in a single subdirectory sequentially with one
> > another (because some depend on files in other subdirectories, which
> > themselves depend on other files in this subdirectory), without errors
> about
> > multiply named modules.
> >
> > Can anyone help me figure out how to do this?
> >
> > Thanks,
> > Jason
>