The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

2010/12/2 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.

So do I. I like the solution but adding pseudo targets for tens of
files is tedious. Maybe these can be added automatically?

> 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.


a -dont-build-proofs option for coq (with a big warning)?


PC