The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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