The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

[firstorder] is quite efficient by itself, however it calls [firstorder auto with *] by default which is almost always a bad idea. You can use the (undocumented but will be in a minute) Set Firstorder Solver option to set it to a more reasonable default tactic.

Best,
-- Matthieu

Le mer. 17 juin 2015 à 09:09, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

P.S.:

 

and of cause in large developments, make -j <#threads> is your friend. I found that the file dependency handling and parallel make robustness of Coq is superior to most C/C++ tool chains I have been working with so far. Up to now I didn’t have any issues with parallel makes with Coq.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Soegtrop, Michael
Sent: Wednesday, June 17, 2015 9:00 AM
To: coq-club AT inria.fr
Subject: RE: [Coq-Club] Coq CPU recommendations

 

Dear Coq Users,

 

actually Coq/CoqIDE 8.5 does several proofs in one file in parallel. I don’t know how it works exactly. It looks like it first parses the Coq file and loads the libraries and then runs several Coqtops in parallel to proof several theorems in parallel. I didn’t figure out as yet how the dependency handling works. Sometimes I have the impression it starts proofs down in the file before proofs it depends on are done. Maye it assumes that opaque dependencies can be proved and discards dependents later in case this is not so.

 

Also you can work on interactively while it is doing proofs.

 

Last but not least the native code compilation of Gallina introduced in Coq 8.5 gives a major speed improvement in certain applications.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of George Van Treeck
Sent: Tuesday, June 16, 2015 11:33 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq CPU recommendations

 

I'm using a 6 core, i7-5930K 3.5GHz with 32G of 2133GHz memory with an SSD drive. It never uses more than 10% of the CPU and 10% of the disk IO when loading libraries and proving files taking about 20 seconds. This might be because Coq does not distribute processing across CPUs much. I didn't see the system creating many new threads when it was loading/proving.  Even with this system's fast memory and an SSD drive, it appears to be little more IO bound than CPU bound. The CoqIDE does not seem to use more than a few hundred MB of memory for what I'm doing. I'm not a professional Coq user. But, I would be surprised if anyone is using more than 4G of memory for Coq. My guess is that even a low end i7 with fast disk drives would suffice. Maybe someone with an i7 laptop and SSD drives can speak to that? I wonder if the Coq development team has a suite of performance benchmarks that can be downloaded for people try on various configurations.

 

-George

 

 

On Tuesday, June 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-----