The Coq mailing list

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

On 06/16/2015 05:33 PM, George Van Treeck wrote:

But, I would be surprised if anyone is using more than 4G of memory for Coq.

My collaborators (the original poster is one of them) and I work on Coq developments in a fairly unusual style, pushing the limits of proof automation.  In that style, it's not too hard to wind up with one source file that, compiled by Coq without using parallelism, uses 20 GB or more.  We at least need 16 GB of RAM available to avoid needing to waste time on too much memory optimization during the initial exploratory stages of a new proof.