The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello, I see two reasons why people don't use coq_makefile as you
want, one bad and one good.

The bad reason is the usual "people are used to make" problem... A lot
of people want to have a fixed makefile, because they know how it
works (that is in a bad but known and stable way). They tend to use
coq_makefile as a "once and for all" tool, then they patch there
Makefile by hand.

The good reason is that people want to add there own rules to the
makefile. I mean non standard ones, like

make distrib
make publishtotheweb
make mybench
make whatever
etc

There are many ways to achieve this, but combined to the bad reason
above, I think it will be hard to make people change there way of
doing this.

P.

2012/12/7 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.