The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi. Your problem does not seem to have any link with emacs or Proofgeneral. The _CoqProject file has been made by the coq team to ease the generation of Makefiles. It happens that it was so useful that Proofgeneral now use it too to guess coqtop options but it is independent from make.

Concerning your problem I am far from a computer right now but did you rename module names according to the new directory? Require skeleton.Mod1. Must be rewritten into Require skeleton.Blah.Mod1. Otherwise the build mechanism may be broken.

Hope this helps.

Pierre

Le dimanche 26 octobre 2014, Craig McLaughlin <mr_mcl AT live.co.uk> a écrit :

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