The Coq mailing list

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

Hi list,

coq_makefile is not used as I imagine to will be when I rewrote a part of it.

How it was imagined :
A user contribution vertionned controlled repertory follows the scheme :
TheName
|_ src/
|  |_.ml{,i,4,lib,pack} files possibly sorted in subdirectories
|_ theories/
|  |_.v files sorted in subdirectories
|_ test-suite/
|  |_files
|_ Make
|_ README
|_ I don't know

The "Make" file contains
-8<---
-I src
-I test-suite
-R theories TheName
-arg (* arguments to send to coqc including *)
-arg -R a_custom_path AContribIDependOn

(*-custom and customized VARIABLES *)

the exhaustive list of .{v,ml{,i,6,lib,pack}} files that are part of the 
contribution one by line
-8<----

A new follower/contributor has to do "coq_makefile -f Make -o Makefile" once 
after its checkout/clone/... 
But then
- Custom targets are accessible directly
- Makefile is regenerated when Make changes(without disturbing the 
git/svn/hg/...),
- Coqide (if it is setup to) will read the Make file and add the -I -R 
-arg_argument automatically when it will start a coqtop 

How it is used :
there is a Makefile in the repository that says something like
-8<----
FILES:=...
NAME:=...

Makefile.coq: Makefile
        $coq_makefile -R . $(NAME) $(FILES) -o $@

all: Makefile.coq
        +$(MAKE) -f $<
-8<----

In the best case there is at the end an :
-8<---
%: Makefile.coq
        +$(MAKE) -f $< $@
-8<---

the reason for that is it to hide the use of coq_makefile and allow a direct 
"make" when the contrib is get from its versionned repository.

So my question is : do you have arguments to use the second setting ? and if 
so how coq_makefile could be made better  in that purpose (generating a 
Makefile.coq that could be "-include Makefile.coq" or it is worst, you don't 
care about the Make file as a project file (you use emacs anyway ()), ...) ?

Pierre B.