[isabelle] Dedicated proof box
In our research group, we are currently considering getting a dedicated
machine for working on proofs. Our Psi-calculus theories are large
enough to incur significant waiting times whenever we have to restart
the proof process. And there is more than one of us now, so simply
getting powerful laptops is looking like the more expensive option.
So I am trying to find out what kind of setup is most effective for
cutting proof times, since a dedicated box gives us a few interesting
options for costumisation.
This paper presents some graphs that show performance benefits declining
somewhat after the 4th core (as is also the case with many other
Since we are two Isabelle-guys now, and will probably be one or two more
in the future, I am considering going for a box with 6-8 cores in total.
And since I read from a previous post on this list that there is an
additional memory-overhead for each core, that would likely put us at 16
or 24GB memory for those cores.
We could also go for a single 8-12 core Opteron, but since it seems that
Xeon cores are fewer in number, though more powerful, the better idea
may be to go for two 4-core or one 6-core Xeon.
But one thing that worries me a bit in that case is Intel's
hyperthreading. So even if we get a 4-core Xeon, it would likely happily
run 8 threads at once, thus potentially doubling the memory requirement
and at the same time flattening the multicore-benefit curve quicker.
And in that case, maybe we should consider just having more real cores
in a single Opteron?
Any thoughts on this would be appreciated. Particularly if someone has
practical experience with running Isabelle on these architectures.
This archive was generated by a fusion of
Pipermail (Mailman edition) and