[isabelle] Engineering Workstation for Isabelle

Dear Isabelle users,

I mentioned my great new Engineering Workstation for Isabelle, and was
asked to say more about it:

  * CPU: Intel i7-9700K 3.6GHz (4.9 GHz turbo), 8 Cores, no
hyperthreading, 12 MB cache

  * RAM: 2 * 16 GB at 3.6GHz

  * persistant storage: 1000 GB Samsung EVO Plus (NVMe PCIe)

  * graphics: Nvidia GT 1030 with passive cooling (UHD: DisplayPort at
60Hz + HDMI at 30Hz)

  * OS: Linux preinstalled (Ubuntu Budgie)

Total price: 1410 EUR before VAT, 1670 EUR with VAT -- by a local Linux
Hardware provider. (I've even met them today at the Linux and Opensource
conference in Augsburg.)

The CPU is very fast and very hot, only the Intel i9-9900K model is even
hotter (Intel tries to compete with AMD again.) It means that running 8
cores in full turbo mode consumes a lot of power and makes quite some
fan noise: so I have switched off the turbo in the BIOS and only use it
in regular 3.6GHz mode; this fits nicely to the extra-fast memory at the
same speed. Thus the fan is almost off under normal circumstances, and
becomes barely audible when "isabelle build -a" starts to crunch.

The persistant storage helps to speed up loading of these ultra-fat JVM
artifacts that we are running with Isabelle/jEdit. It also helps a lot
for stored heap images of Poly/ML. (I would never go back to an actual

The extra graphics card (80 EUR) could have been omitted: that Intel CPU
has quite capable UHD graphics on-chip, but the mainboard exposed it
only as HDMI (30Hz), not as DisplayPort (60Hz) for my fancy Samsung UHD
display (300 EUR in 2018, 250 EUR in 2019).

Here are some adhoc numbers from "isabelle build -g main" (approximately
at Isabelle2019-RC0):


  ML_OPTIONS="--minheap 1500"

Finished HOL (0:02:12 elapsed time, 0:06:43 cpu time, factor 3.05)
Finished HOL-Analysis (0:04:09 elapsed time, 0:18:37 cpu time, factor 4.48)
Finished HOL-Library (0:01:05 elapsed time, 0:05:01 cpu time, factor 4.60)
Finished HOL-Computational_Algebra (0:00:36 elapsed time, 0:01:44 cpu
time, factor 2.89)
Finished HOL-Algebra (0:00:40 elapsed time, 0:03:33 cpu time, factor 5.24)
Finished HOL-Probability (0:00:39 elapsed time, 0:03:14 cpu time, factor
Finished HOL-Number_Theory (0:00:30 elapsed time, 0:02:11 cpu time,
factor 4.33)

I will try this again tomorrow, with all 8 cores, and also with this
hot/noisy turbo mode.

(The above looks already like an invitation to Larry to port even more
HOL-Analysis stuff by John Harrison :-)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.