The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

AUGER Cedric wrote:
> I guess you meant coqide; you also should be more precise on the
> problem you were trying to solve. Taking 1 or 2 minutes, is really a
> bad omen.
>    

I disagree, though it depends on the sense of "bad omen." ;)  It's easy 
for proof scripts that use a lot of automation to run for hours and use 
tens of gigabytes of RAM.