The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

Here's a question this thread begs: how cache efficient does Coq wind up being? Like, internally is it just creating tons of copy-on-write structures? How smart is it about reusing objects which are due to fall out of scope (think temp values constructed during reductions)?

Could be the cache barely matters, if the allocation/reuse strategy is too simple.

On Jun 17, 2015 11:52 AM, "Timothy Carstens" <intoverflow AT gmail.com> wrote:

This is why I recommend going with quad-channel DDR. Anything less is gamer/homework grade. If you're doing gigs of symbolic computation, and especially if you're going multi-core, the extra memory bandwidth is a must.

And don't overclock your memory, itll drive up your bandwidth but also wreck you latency. Most of your memory operations will be to/from CPU cache (versus memcopies via PCIe go a peripheral) so you will be doing relatively small burst read/write, and thus need low latency RAS/CAS settings for your memory (hard to do when overclocked).

-t

On Jun 17, 2015 10:49 AM, "Adam Chlipala" <adamc AT csail.mit.edu> wrote:

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.