The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

AUGER Cedric wrote:
> Furthermore, I never consider proof scripts running for hours, since
> that means for me that they are "one shot" proofs. I cannot wait hours
> each time I want to modify a bit of the developpement.
>    

I would argue that this is a superior choice to spending even longer 
writing the script in the first place, or figuring out how to adapt it 
when you change the theorem.  Person-hours matter more than CPU-hours!

Eventually, this should all be sped up by multi-core parallelization of Coq.