Email Gateway (Aug 22 2022 at 16:00): Email Gateway (Aug 22 2022 at 16:00):From: "Jähnig, Nils Erik" <nils.jaehnig@tu-berlin.de>
Thank you all for your feedback.
It seems like 8 cores should be fine for non-AFP, interactive theory development, preferably with a high frequency.
When I get around to buy a machine, I will report back.
Nils
Email Gateway (Aug 22 2022 at 16:09):From: "Jähnig, Nils Erik" <nils.jaehnig@tu-berlin.de>
Dear Isabelle users,
I can buy a new machine for work :)
I wonder how many cores are useful for theory development in Isabelle.
And does anyone have experiences with high-end computer for this purpose?
I would be glad if some peaple could share their setups.
(plus points for hackintosh compatibility, but linux is of course fine)
Have a nice weekend
Nils
Email Gateway (Aug 22 2022 at 16:09):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Nils,
I have a laptop with 8 CPUs (with hyperthreading) and 16GB of RAM
(running linux).
My setup is (in Isabelle's etc/settings file):
ISABELLE_BUILD_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
ISABELLE_BUILD_OPTIONS="threads=8"
ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 1500 --gcthreads 4"
For some of our sessions I get a speedup close to 8.
However, with this setup my laptop is almost unusable for other stuff
during build time. That is why I usually build heap images on a remote
workstation and then rsync them over to my laptop (just 2 weeks ago
Makarius helped me to write an Isabelle tool that automates this, in
case anybody is interested; currently this "heap_copy" tool---which
should rather be named "remote_build"---is part of IsaFoR).
The workstation has 12 CPUs (6 physical cores + hyperthreading) and 32GB
of RAM and as a corollary our setup is:
ISABELLE_BUILD_OPTIONS="threads=12"
ISABELLE_BUILD_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 1500 --gcthreads 6"
In both cases I use 64bit Poly/ML (via changing ML_HOME) since IsaFoR
needs more RAM than can be addressed with the 32bit version. If you do
not need 64bit, don't do this, since 32bit Poly/ML is probably around
twice as fast.
With this setup we sometimes (rarely) see a speedup around 9. So at
least for IsaFoR it seems that up to 8 CPUs are really useful (of
course if you also want to work on the same machine, more would be
better ;)).
hope this helps
chris
Email Gateway (Aug 22 2022 at 16:10):From: Lars Hupel <hupel@in.tum.de>
Hi Nils,
the more, the merrier :-)
I personally compute on a recent 4 core + HT laptop (32 GB) and at home
on a somewhat dated 4 core + HT desktop (also 32 GB). Both are fine for
interactive development of medium-sized applications (~ 10k–20k lines).
If you frequently change stuff that comes early in the session graph and
find yourself rebuilding things like HOL-Probability (or the AFP even)
often, I would recommend at least 8 cores.
For continuous builds we use a total of 22 cores which can be saturated
by the AFP very easily.
All of the above concerns Linux.
For Mac, well, you're pretty much out of luck without Hackintosh. Not
sure what hardware would work with that though.
Cheers
Lars
Last updated: Apr 25 2024 at 01:08 UTC