The Coq mailing list

[rabforum <rabforum AT ukr.net>]

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 "=". And 
coq_makefile doesn't replace Makefile-s in subdirectories.

After all, this way or another, problem is solved.