The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

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.  I always use coq_makefile to calculate the dependencies, 
which is quite convenient.

In practice, what I do is run 'make' and stop when I see the file I'm 
working on start compiling.  When there are long-running but unrelated 
jobs that would naturally run first, I make their long-running proof 
scripts 'Admitted', temporarily commenting out the real code.  Clearly 
an ugly solution, but it gets the job done; niftier tool support would 
be welcome.