coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Coq CPU recommendations
- Date: Wed, 17 Jun 2015 07:00:04 +0000
- Accept-language: de-DE, en-US
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
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:
|
- [Coq-Club] Coq CPU recommendations, Benjamin Barenblat, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, Eric Mullen, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, Eric Mullen, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, Adam Chlipala, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, Eric Mullen, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, George Van Treeck, 06/16/2015
- RE: [Coq-Club] Coq CPU recommendations, Soegtrop, Michael, 06/17/2015
- RE: [Coq-Club] Coq CPU recommendations, Soegtrop, Michael, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Enrico Tassi, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Matthieu Sozeau, 06/17/2015
- RE: [Coq-Club] Coq CPU recommendations, Soegtrop, Michael, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Adam Chlipala, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Pierre-Marie Pédrot, 06/18/2015
- Re: [Coq-Club] Coq CPU recommendations, David MENTRE, 06/18/2015
- RE: [Coq-Club] Coq CPU recommendations, Soegtrop, Michael, 06/18/2015
- Re: [Coq-Club] Coq CPU recommendations, Adam Chlipala, 06/18/2015
- Re: [Coq-Club] Coq CPU recommendations, Pierre-Marie Pédrot, 06/18/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/17/2015
- RE: [Coq-Club] Coq CPU recommendations, Soegtrop, Michael, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, Eric Mullen, 06/16/2015
Archive powered by MHonArc 2.6.18.