[isabelle-dev] isabelle build timing

Makarius makarius at sketis.net
Sat Sep 2 16:21:08 CEST 2017

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.




  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)

More information about the isabelle-dev mailing list