The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

rabforum wrote:
> Adam Chlipala wrote:
> > rabforum wrote:
> > > I'm actually trying to run one of Coq's contributions, Constructive 
> > > Category Theory http://coq.inria.fr/contribs/category.html . I want 
> > > to use a hierarchical module names, like in this letter about CoLoR: 
> > > http://pauillac.inria.fr/pipermail/coq-club/2008/003746.html . 
> > > Unforunatily coq_makefile don't produce Makefile that gives to coqc 
> > > '-R' option even if I give '-R' option to coq_makefile. So instead 
> > > of using make I have written a Haskell script that compiles files in 
> > > a folder and its subfolders in no particular order. Of cause, my 
> > > script yields errors because of dependencies. So I repeat my script 
> > > until it yields zero errors.
> > >
> > > Is there an easy way, special tools etc.?
> >
> > There is a manual-ish way that still lets you use coq_makefile to do 
> > most of the work.  You can run it like:
> >    coq_makefile A.v COQC="coqc -R B C" COQDEP="coqdep -R B C"
> >
> > Modify the alternate command line prefixes suggested to include 
> > whatever switches you need for your build process, including [-R] 
> > path mappings.
> I run this command and its variations.
> $ coq_makefile `cat Make` -I . -R . COQC = "coqc -R . category_theory" 
> COQDEP = "coqdep -c -R . category_theory" -o Makefile
> Regretfully it does not work. Sometimes coq_makefile treats variables 
> in command line (COQC = ...) as variables and sometimes as 
> subdirectories. It matters whether spaces are in between "COQC" and "=".

Yes, like in my example, I always leave out spaces.  What's wrong with 
doing that?

> And coq_makefile doesn't replace Makefile-s in subdirectories.

That's true, but the generated Makefiles _will_ build .vo files from .v 
files in other subdirectories, even if the importance of those .vo files 
is only inferred by dependency analysis, and even if you don't mention 
those other files directly in your Makefile.  Thus, it tends to work out 
fine for me in practice.