The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I generally find that 32 GB is uncomfortably little RAM to have on hand 
for the sorts of Coq proofs that I tend to write, especially during a 
parallel build.

On 04/27/2018 11:31 PM, Clément Pit-Claudel wrote:
> On 2018-04-27 19:59, Jim Fehrle wrote:
> > >   fortunately, my VST proof development is itself much more efficient, so 
> > > therefore I can do big things with a large collection of .v files that /each/ 
> > > take no more than 1 gigabyte (and usually much less) to process with coqc.
> > Sounds like a memory leak.
> 1GB actually sounds like a very typical memory footprint for a large Coq 
> proof, in my experience.  It's not uncommon to grow to 10 or 15GB for larger 
> ones.