[isabelle-dev] Isabelle build timing on high-end hardware

[Makarius]

On 02/07/18 15:21, Makarius wrote:
> 
> 2 * Intel(R) Xeon(R) Gold 6148 CPU @ 2.40GHz;
> 2 NUMA nodes: distance factor 2.1 for memory access;
> each CPU with 20 cores and hyper-threading: total of 80 hardware threads
> 
> 256 GB SSD
> 
> Ubuntu Linux 16.04

Here are more timing results on that great machine of some Isabelle users:

  ML_PLATFORM="x86-linux"
  ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.7.1-8/x86-linux"
  ML_SYSTEM="polyml-5.7.1"
  ML_OPTIONS="--minheap 1500"

Isabelle/8ef8905629ba
AFP/234a91c26d02
isabelle build -o threads=6 -j10 -a -N -d '$AFP' -f -x HOL-ODE-Numerics
-X slow
0:36:19 elapsed time, 19:13:18 cpu time, factor 31.75


Note that the sessions starting from HOL-ODE-Numerics are relatively
slow, but insignificant for a meaningful test: ignoring them like the
"slow" group leads to very good results, below the critical "Paris
Commuter constant".

It is even slightly better than the 45min from 2012, when "isabelle
build" was new and that expression came up in Paris Sud. Shortly
afterwards we've had a lot of activity on Isabelle + AFP, as a
consequence of renovations of Isabelle/Pure/HOL + libraries -- when
testing was fun.


	Makarius