[isabelle-dev] Slow builds due to excessive heap images

[Makarius]

We are presently testing Poly/ML 5.7.1 by default (see
Isabelle/aefaaef29c58) and there are already interesting performance
figures, e.g. see:

http://isabelle.in.tum.de/devel/build_status
http://isabelle.in.tum.de/devel/build_status/Linux_A
http://isabelle.in.tum.de/devel/build_status/AFP

Overall, performance is mostly the same as in Poly/ML 5.6 from
Isabelle2017, but there are some dropouts. In particular, loading heap
images has become relatively slow: this impacts long heap chains like
HOL-Analysis or big applications in AFP. E.g. see
http://isabelle.in.tum.de/devel/build_status/AFP/index.html#session_CAVA_LTL_Modelchecker
(timing vs. ML timing).

I've shown this to David Matthews already and await his answer. It could
be just an accident in Poly/ML 905dae2ebfda or inherent due to the new
heap + GC management that is more robust against out-of-memory failures.


Independently of that, excessive use of intermediate heap images makes
builds much slower than necessary, because multithreading is reduced by
the structural serialization. Here is a typical example:

Isabelle/4ff031d249b2
AFP/4482dd3b0471

ML_PLATFORM="x86_64-linux"
ML_HOME="/home/wenzelm/.isabelle/contrib/polyml-test-905dae2ebfda/x86_64-linux"
ML_SYSTEM="polyml-5.7.1"
ML_OPTIONS="--minheap 1500"

$ isabelle build -o threads=6 -d '$AFP' -f Linear_Recurrences_Test
Finished Pure (0:00:18 elapsed time, 0:00:17 cpu time, factor 0.96)
Finished HOL (0:03:32 elapsed time, 0:10:48 cpu time, factor 3.06)
Finished HOL-Library (0:02:04 elapsed time, 0:08:12 cpu time, factor 3.94)
Finished HOL-Computational_Algebra (0:01:11 elapsed time, 0:02:51 cpu
time, factor 2.39)
Finished HOL-Algebra (0:02:01 elapsed time, 0:04:51 cpu time, factor 2.41)
Finished JNF-HOL-Lib (0:00:43 elapsed time, 0:00:55 cpu time, factor 1.26)
Finished JNF-AFP-Lib (0:02:14 elapsed time, 0:07:32 cpu time, factor 3.37)
Finished Jordan_Normal_Form (0:06:54 elapsed time, 0:16:29 cpu time,
factor 2.38)
Finished Subresultants (0:03:00 elapsed time, 0:04:28 cpu time, factor 1.49)
Finished Pre_BZ (0:03:56 elapsed time, 0:08:15 cpu time, factor 2.09)
Finished Berlekamp_Zassenhaus (0:05:41 elapsed time, 0:11:14 cpu time,
factor 1.98)
Finished Pre_Algebraic_Numbers (0:05:02 elapsed time, 0:05:41 cpu time,
factor 1.13)
Finished Algebraic_Numbers_Lib (0:05:51 elapsed time, 0:08:07 cpu time,
factor 1.39)
Finished Linear_Recurrences (0:06:28 elapsed time, 0:07:11 cpu time,
factor 1.11)
Finished Linear_Recurrences_Test (0:08:24 elapsed time, 0:13:41 cpu
time, factor 1.63)
0:57:59 elapsed time, 1:50:38 cpu time, factor 1.91

That looks impressive, but there is not so much behind it. When
Linear_Recurrences_Test uses "HOL" as parent and "Linear_Recurrences" as
import session (see ch-test) the timing becomes:

$ isabelle build -o threads=6 -d '$AFP' -f Linear_Recurrences_Test
Finished Pure (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.95)
Finished HOL (0:03:31 elapsed time, 0:10:32 cpu time, factor 2.99)
Finished Linear_Recurrences_Test (0:08:20 elapsed time, 0:37:48 cpu
time, factor 4.53)
0:12:31 elapsed time, 0:48:38 cpu time, factor 3.88

$ isabelle build -o threads=12 -d '$AFP' -f Linear_Recurrences_Test
Finished Pure (0:00:15 elapsed time, 0:00:14 cpu time, factor 0.95)
Finished HOL (0:03:25 elapsed time, 0:12:12 cpu time, factor 3.56)
Finished Linear_Recurrences_Test (0:06:31 elapsed time, 0:39:11 cpu
time, factor 6.00)
0:10:34 elapsed time, 0:51:38 cpu time, factor 4.89


I still have some ideas for "isabelle build" in the pipeline (for
several years) to skip building intermediate heaps in the first place.
Then AFP (without the "slow" sessions) could shrink to 50% .. 20% build
time.

Until that emerges, AFP contributors may want to double-check, which
auxiliary heaps ("Base", "Lib", "Pre") are really needed and beneficial
for overall build times.

Just for private development, it is always possible to specify auxiliary
sessions in $ISABELLE_HOME_USERS/etc/ROOT and comment them in or out on
demand. This simplifies the structure of the published AFP and makes
builds faster right now without further technology. Session-qualified
theory names allow this flexibility already.


	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1509220282 -7200
#      Sat Oct 28 21:51:22 2017 +0200
# Node ID 8d81720c2abab7677d00df167eba65341a302393
# Parent  4482dd3b04713302842a538c42902d2198ceab14
test

diff -r 4482dd3b0471 -r 8d81720c2aba thys/Linear_Recurrences/ROOT
--- a/thys/Linear_Recurrences/ROOT	Sat Oct 28 19:14:14 2017 +0200
+++ b/thys/Linear_Recurrences/ROOT	Sat Oct 28 21:51:22 2017 +0200
@@ -10,7 +10,9 @@
   document_files
     "root.tex"
 
-session Linear_Recurrences_Test (AFP) = Linear_Recurrences +
+session Linear_Recurrences_Test (AFP) = HOL +
   options [document = false, timeout = 600]
+  sessions
+    "Linear_Recurrences"
   theories
     Linear_Recurrences_Test