Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq CPU recommendations

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq CPU recommendations


Chronological Thread 
  • From: Timothy Carstens <intoverflow AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Coq CPU recommendations
  • Date: Wed, 17 Jun 2015 11:52:40 -0700

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.



Archive powered by MHonArc 2.6.18.

Top of Page