[isabelle-dev] isabelle build timing

[Makarius]

Here is some timing information for standard variations on "isabelle
build -a", see details below.

The hardware is lxcisa0 at TUM, which is an Intel Xeon with many cores.
(Lars Hupel can explain the precise hardware setup).


The canonical build parameters for this machine appear to be:

  isabelle build -j8 -o threads=6

Summary of results:

  * Isabelle: 16.5 min
  * Isabelle + AFP (without slow): approx. 1h
  * AFP alone (without slow): approx. 50 min
  * AFP alone (without very_slow): approx. 2h


Thus we are back to the fairly good situation of 2012/2013, when Damien
Doligez invented the term "Paris commuter's constant" (of 45min), for
the time one can sit and wait for AFP builds. In contrast, the slow
build of 2h requires a full French lunch time.

I have still some ideas in reserve to speed this up further. But right
now we are already at the biggest builds and fastest build times ever,
and throwing even more cores at it could improve it without further ado.


	Makarius

------------------------------------------------------------------------

Isabelle/19bf4d5966dc
AFP/419b0f1b9088

  ML_PLATFORM="x86-linux"
  ML_HOME="/home/isabelle/contrib/polyml-5.6-1/x86-linux"
  ML_SYSTEM="polyml-5.6"
  ML_OPTIONS="--minheap 1600"


isabelle build -j8 -o threads=6 -a
0:16:26 elapsed time, 4:19:17 cpu time, factor 15.77

isabelle build -j8 -o threads=8 -a
0:16:30 elapsed time, 4:10:58 cpu time, factor 15.20

isabelle build -j10 -o threads=6 -a
0:16:57 elapsed time, 4:19:36 cpu time, factor 15.31


#based on existing Isabelle build
isabelle build -j8 -o threads=6 -d '$AFP' -a -X slow
0:49:40 elapsed time, 16:20:11 cpu time, factor 19.73

#based on existing Isabelle build
isabelle build -j8 -o threads=6 -d '$AFP' -a -X very_slow
...
Finished ConcurrentGC (1:17:09 elapsed time, 4:05:13 cpu time, factor 3.18)
Finished AODV (1:44:30 elapsed time, 6:55:36 cpu time, factor 3.98)
2:00:08 elapsed time, 32:48:01 cpu time, factor 16.38


#fresh build
isabelle build -j11 -a -d '$AFP' -X slow
0:58:53 elapsed time, 19:52:46 cpu time, factor 20.25

#fresh build
isabelle build -j8 -o threads=6 -a -d '$AFP' -X slow
1:02:40 elapsed time, 20:04:21 cpu time, factor 19.22

isabelle build -j8 -o threads=6 -d '$AFP' -g slow
Finished Iptables_Semantics_Examples (0:39:33 elapsed time, 2:07:06 cpu
time, factor 3.21)
Finished JinjaThreads (0:46:58 elapsed time, 2:58:39 cpu time, factor 3.80)
Finished ConcurrentGC (1:11:03 elapsed time, 4:44:22 cpu time, factor 4.00)
Finished AODV (1:30:52 elapsed time, 7:11:01 cpu time, factor 4.74)
Finished Flyspeck-Tame (4:52:25 elapsed time, 7:28:22 cpu time, factor 1.53)
------------------------------------------------------------------------