The Coq mailing list

[Hendrik Tews <tews AT os.inf.tu-dresden.de>]

Adam Chlipala 
<adam AT chlipala.net>
 writes:

   Hendrik Tews wrote:
   > This is not too difficult. Just use a pseudo goal, which depends
   > on the real things. eg
   >
   > buf1.pseudo: buf2.vo ...
   >
   > and in buf1.v you include at the end
   >
   > (*** Local Variables ***)
   > (*** compile-command: "make buf1.pseudo" ***)
   > (*** End: ***)
   >    

   This solution has the drawback of forcing you to declare dependencies
   explicitly.

No, I only explained the general idea. To integrate with
coq_makefile, you take a Makefile with

include coq-makefile

%.v.d: %.v
        $(COQDEP) -slash $(COQLIBS) "$<" > "$@" \
                && echo ".PHONY: $<.dependencies" >> "$@" \
                && $(COQDEP) -noglob -slash $(COQLIBS) "$<" | \
                                sed "s/^.*: $< /$<.dependencies: /" >> "$@" \
                || ( RV=$$?; rm -f "$@"; exit $${RV} )

and save the output of coq_makefile into coq-makefile. The rule
above will then generate .PHONY x.v.dependencies targets.

Patching coq_makefile to generate those dependency targets would
of course be much simpler.

Bye,

Hendrik