The Coq mailing list

[Jasper Stein <jasper AT cs.kun.nl>]

Sébastien Hinderer wrote:
> Hi,
>
> I have to write a set of compilation scripts for a project that has crossed
> dependencies over directories:
> the project consists of more directories, each of them containing more .v
> files. However, it is not possible to compile the directories one after the
> other, since the dependencies don't respect the directory structure.
>
> So I presume that coq_makefile is not general enough, since its "depend"
> rule looks for dependencies on "*.v", where I would need a recursive search
> of *.v files.
>
> Am I right or is there another solution ?

What may work (but it may not be the most elegant solutions in all 
cases) is to tweak your .coqrc file(s). If you add a line

Add Rec "/some/dir/"

then every subdirectory will be searched when Coq encounters a command 
Require blah. I'm not sure if coqdep or coq_makefile also pick these up, 
but you may try anyway.

Jasper
--
Het verschil tussen theorie en praktijk is dat in theorie
er geen verschil is tussen theorie en praktijk.