The Coq mailing list

[Gyesik Lee <gslee AT hknu.ac.kr>]

Many thanks for the reply.

Let me make my question more concrete.

Assume in a directory called foo I have the coq files A1.v, A2.v.

And there is a subdirectory called foo_sub where B1.v, B2.v B3.v are contained.

Furthermore, A1.v and A2.v depend on files B1.v, B2.v, and B3.v.

My question was: how to create Makefile using coq_makefile such that I just need to type "make" to compie A1.v and A2.v?

(that is all the files in the foo directory)

If there is no dependency involving subdirectories or other directories, I used to do the following:

coq_makefile *.v > Makefile

and just type "make" to compile all the files.

I hope my question is this time clearer.

Gyesik

2012/2/22 Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>

Hi,
I do not understand what you want.

Is it
I've got A.v, foo/B.v, foo/C.v where A Requires Foo.B and B Requires Foo.C.
I write

-R . toto
A.v

in my _CoqProject file. I do coq_makefile -f _CoqProject -o Makefile
and I expect everything to work ?

This will not because of dependencies; only the one of listed files are compute so you will have
A.vo: foo/B.vo
but nothing that say
foo/B.vo: foo/C.vo
and C will no be compiled.

I may complitely miss the point and, because I need to rewrite coq_makefile documentation, I'm interressted to get more information.

All the best,
Pierre Boutillier

Le 22 févr. 12 à 04:22, Gyesik Lee a écrit :

Hi,

would someone remind me of how to create Makefile such that all the dependent files in subdirectories or special directories can be automatically involved during compilation?

I tried to follow the instructions from the coq_makefile --help, but failed.

Any help would be appreciated.

Gyesik