The Coq mailing list

[Craig McLaughlin <mr_mcl AT live.co.uk>]

Hi all,

I was wondering if anyone knew how to correctly manage dependencies within
a Coq project using _CoqProject with Emacs? Here are the details:

I'm using the repository https://github.com/thoughtpolice/coq-skeleton as a
test and the setup works fine as is. However, I run into some issues 
with the
build process when I move the files Mod1.v and SfLib.v into a subdirectory.
I have _CoqProject as:

-R . Skeleton
./CpdtTactics.v
./ExtractHaskell.v
./ExtractOcaml.v
./Main.v

and I've created a subdirectory called ``Blah'' which contains Mod1.v and
SfLib.v. Now, when I perform coq_makefile -f _CoqProject -o Makefile 
then make
tries to compile Mod1.v first (before CpdtTactics and SfLib, its
dependencies). However, if I just have Mod1.v in the ``Blah'' subdirectory
(i.e. place SfLib.v in the outer directory), the process above builds the
modules in the correct order. Any ideas why this doesn't work with 
SfLib.v in
the subdirectory?

The only solution I have come across is by specifying both ./Blah/Mod1.v and
./Blah/SfLib.v in the _CoqProject file but I would rather not have to do 
this
since my actual project has many files within the subdirectory.

Let me know if I have missed anything from the relevant documentations 
of Coq
or Proof General, but as far as I can discern I have not.

For convenience, I have forked the repository with my changes committed,
available here: https://github.com/cmcl/coq-skeleton.git

Regards,
Craig