The Coq mailing list

[Gyesik Lee <leegys AT gmail.com>]

Dear Pierre,

thank you for your help. 

(I am using Emacs with proofgeneral in linux or os x environment.)

I didn't know that in the reference of V8.4beta a more detailed explanation about coq_makefile is made than before.

Anyway, both manual versions works great.

But I don't understand how to use the following really "FANCY" style which is also explained in the reference.

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

Please excuse my ignorance, but when I just did copy-and-paste that line into the Terminal, then I was prompted by "<" symbol expecting some inputs.

I don't know what to do then.

Would you give more explanation?

Gyesik

 

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