The Coq mailing list

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

The [abstract] tactical provides a generic way of reducing that memory overhead, by periodically forcing all of the closures into proof terms.  It can have major effects on memory usage.

On 06/16/2015 01:32 PM, Timothy Carstens wrote:

I think the issue is that the tactics engine builds loads of closures as it tries things out. (Is that right?) If so, that's hard to meaningfully optimize, unless there's a systemic way to make far fewer of 'em.

On Jun 16, 2015 10:17 AM, "Eric Mullen" <emullen AT cs.washington.edu> wrote:

I've discovered myself writing proofs differently in order to make them run faster/use less memory. I wonder if it would be possible to develop a tactic optimizer (a la query optimizer from DB) which could optimize a long chain of semicolon strung together tactics to run faster/use less memory.

Mostly I've found that simpl is slower than you think, and firstorder is almost always a terrible idea.

Eric

On Tue, Jun 16, 2015 at 10:12 AM Timothy Carstens <intoverflow AT gmail.com> wrote:

Maximize your cache and get a CPU that supports quad-channel DDR, as there's symbolic things going on. Either Xeon (not worth it unless you are going for max parallelism) or an i7-extreme (which is a Xeon with some cores fuse-disabled). I have run out of memory with 64GB installed, so YMMV.

On Jun 16, 2015 10:05 AM, "Eric Mullen" <emullen AT cs.washington.edu> wrote:

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-----