The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Tue, 02 Aug 2011 08:43:21 -0400,
Adam Chlipala 
<adam AT chlipala.net>
 a écrit :

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

Precisely, the machine in which it was supposed to run is a 4Go one;
and as it was not precised 64 bits, I guess it is also a 32 bits one;
so using "tens of gigabytes of RAM" won't work.
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.