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


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
(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:


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

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.

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

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 @@
-session Linear_Recurrences_Test (AFP) = Linear_Recurrences +
+session Linear_Recurrences_Test (AFP) = HOL +
   options [document = false, timeout = 600]
+  sessions
+    "Linear_Recurrences"
isabelle-dev mailing list

Reply via email to