The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

In very durty :

coq_makefile $(find . -type d -exec echo -I \{\} \;) $(find -name \*.v -print) -o Makefile

In less durty :

coq_makefile -R . SuperLib $(find -name \*.v -print) -o Makefile

(but then you'll have to Require Foo_sub.B? in A? files)

and

{ echo ’-R . MyFancyLib ’ ; find -name ’*.v’ -print } > _CoqProject && coq_makefile -f _CoqProject -o Makefile

if you follow what I've written here : http://coq.inria.fr/distrib/V8.4beta/refman/Reference-Manual018.html#toc97

In the last case

 - coq_makefile will be automatticaly called if something change in the _CoqProject file (you add a file or an option)

 - if you use coqide, you can set up it up in order that it does automaticaly the -R . MyFancyLib when you open one of the file listed in the _Coq_project file ...

Pierre

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

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