The Coq mailing list

[Eric Mullen <emullen AT cs.washington.edu>]

I have a dedicated coq machine with an i7-4790K and 16g of ram. It works quite well in practice. Additionally, at UW, we're developing an emacs mode which allows you to edit proof files located on your machine, but running coqtop to process the files on a remote server. We'll post to this mailing list when it's a bit more stable.

In general I'd recommend getting an i7-4790K and at least 8g of ram (16 seems to have been overkill). You might also want to look into overclocking, you can push the i7-4790K up to 5gHz in some cases. I've heard good things about http://siliconlottery.com/ if you're interested in buying a processor for overclocking.

I don't know whether coq is bound more by memory bandwidth or CPU speed, but I do know that in practice my coq server is quite a bit faster than any other machine I have.

I would be very curious as to whether coq is memory or cpu limited.

Eric

On Tue, Jun 16, 2015 at 9:22 AM Benjamin Barenblat <bbaren AT mit.edu> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Hi all,

Does anybody have recommendations for hardware that runs Coq especially
well?  I would like Coq to run as quickly as possible using standard,
commercial off-the-shelf hardware like Intel’s i7-4790K.

I’m also curious about Coq’s CPU cache usage.  When Coq runs slowly, is
it actually CPU-bound, or is it bound by RAM bandwidth?

Thanks in advance,
Benjamin
-----BEGIN PGP SIGNATURE-----

iQF8BAEBCgBmBQJVgEwyXxSAAAAAAC4AKGlzc3Vlci1mcHJAbm90YXRpb25zLm9w
ZW5wZ3AuZmlmdGhob3JzZW1hbi5uZXQ5OThCQjVEMTlDOEE3QjE3OUUwREFCODY5
RTczMDE0OUVCOTFDNTNCAAoJEJ5zAUnrkcU73iIH/iHru9cbiHYPhtBmL577KNhg
hU4dyLHKeBbp4jocj+k5UbxMIvW1HS8QSyEVzN2RzzhSd+YHhIjE7My0qnnycRpk
VqzijnfeKl4m8IHmbi2+WhstZzVp9wWnE9+3HDc3XJV8IGYv2gyAALuy2ma43JmS
RJnqB5m+s4mvejsPCGWkIUxzlIdSi4uarC2WrkFE2vkASgObSc7mBmTLV2iqNmfT
ELaEKYHyWMwBfOGgEgAieoAf4lkz70uKNo/oIRLl53ANIR2X9RbTJboEKxZMMNUk
eu1oVXQeVKKy+mOyCmPexYTXRzl+0WIhjWdz3SO6b3f7ee9TsfwQ2V8EOjaRGSQ=
=qWuU
-----END PGP SIGNATURE-----