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

[Makarius]

On 04/11/17 19:30, David Matthews wrote:
> 
> I've had a look at this and pushed a change to IntInf.pow to Poly/ML
> master (c2a2961).  It now uses Word.andb rather than IntInf.andb which
> avoids a call into the run-time system (RTS).
> 
> However, this code hadn't changed since 5.6 and when I tested it using
> List.map with 5.6 and 5.7.1 I didn't notice much difference; certainly
> not the massive differences you found with Par_List.map.  The only thing
> I can think of is that there were so many calls into the RTS that there
> was some contention on a mutex and that was causing problems.
> 
> Anyway, try the new version and let me know the results.

I have briefly tested the subsequent version Poly/ML 31b5de8ee56 and it
works well with Isabelle/978c584609de + ch-pow and AFP/9ad8f3af760f:

  ML_PLATFORM="x86_64-linux"
  ML_HOME="/home/wenzelm/lib/polyml/x86_64-linux"
  ML_SYSTEM="polyml-5.7.1"
  ML_OPTIONS="--minheap 4G --maxheap 32G"

lxcisa0> isabelle build -d '$AFP' -o threads=8 Lorenz_C0
Building Pure ...
Finished Pure (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.95)
Building HOL ...
Finished HOL (0:03:21 elapsed time, 0:11:15 cpu time, factor 3.35)
Building HOL-Analysis ...
Finished HOL-Analysis (0:05:09 elapsed time, 0:27:51 cpu time, factor 5.40)
Building Ordinary_Differential_Equations ...
Finished Ordinary_Differential_Equations (0:01:55 elapsed time, 0:08:18
cpu time, factor 4.33)
Building HOL-ODE ...
Finished HOL-ODE (0:00:01 elapsed time)
Building HOL-ODE-Refinement ...
Finished HOL-ODE-Refinement (0:03:17 elapsed time, 0:20:01 cpu time,
factor 6.10)
Building HOL-ODE-Numerics ...
Finished HOL-ODE-Numerics (0:18:23 elapsed time, 0:43:51 cpu time,
factor 2.39)
Building Lorenz_Approximation ...
Finished Lorenz_Approximation (0:03:51 elapsed time, 0:08:15 cpu time,
factor 2.14)
Running Lorenz_C0 ...
Finished Lorenz_C0 (0:13:14 elapsed time, 1:39:57 cpu time, factor 7.55)
0:49:55 elapsed time, 3:39:48 cpu time, factor 4.40


Here are also the earlier results with the workaround
(Isabelle/17eb23e43630):

On 03/11/17 20:07, Makarius wrote:
> $ isabelle build -d '$AFP' -o threads=8 Lorenz_C0
> Building Pure ...
> Finished Pure (0:00:16 elapsed time, 0:00:16 cpu time, factor 0.95)
> Building HOL ...
> Finished HOL (0:03:19 elapsed time, 0:10:54 cpu time, factor 3.28)
> Building HOL-Analysis ...
> Finished HOL-Analysis (0:05:16 elapsed time, 0:28:08 cpu time, factor
5.33)
> Building Ordinary_Differential_Equations ...
> Finished Ordinary_Differential_Equations (0:01:59 elapsed time, 0:08:10
> cpu time, factor 4.10)
> Building HOL-ODE ...
> Finished HOL-ODE (0:00:01 elapsed time)
> Building HOL-ODE-Refinement ...
> Finished HOL-ODE-Refinement (0:03:29 elapsed time, 0:20:08 cpu time,
> factor 5.76)
> Building HOL-ODE-Numerics ...
> Finished HOL-ODE-Numerics (0:18:06 elapsed time, 0:41:23 cpu time,
> factor 2.28)
> Building Lorenz_Approximation ...
> Finished Lorenz_Approximation (0:03:43 elapsed time, 0:07:53 cpu time,
> factor 2.12)
> Running Lorenz_C0 ...
> Finished Lorenz_C0 (0:14:21 elapsed time, 1:49:04 cpu time, factor 7.60)
> 0:51:01 elapsed time, 3:45:59 cpu time, factor 4.43


So the uniform use of IntInf.pow might come out slightly faster.

I will make a proper polyml-test component soon and then apply ch-pow
permanently, but it needs a few more days: there is still
NewTestRegisterSave (Isabelle/c70c47dcf63e) in the queue for official
testing and timing -- my impression is that it will be only a few
percent faster.


	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1509824436 -3600
#      Sat Nov 04 20:40:36 2017 +0100
# Node ID 415a6bba9344b53576477a6e03d6ea5f6219ad1d
# Parent  978c584609ded0d1a36246b83aeb8630d14034f9
test

diff -r 978c584609de -r 415a6bba9344 src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML	Sat Nov 04 19:44:28 2017 +0100
+++ b/src/Pure/General/integer.ML	Sat Nov 04 20:40:36 2017 +0100
@@ -40,20 +40,7 @@
 
 fun square x = x * x;
 
-fun pow k l =
-  let
-    fun pw 0 _ = 1
-      | pw 1 l = l
-      | pw k l =
-          let
-            val (k', r) = div_mod k 2;
-            val l' = pw k' (l * l);
-          in if r = 0 then l' else l' * l end;
-  in
-    if k < 0
-    then IntInf.pow (l, k)
-    else pw k l
-  end;
+fun pow k l = IntInf.pow (l, k);
 
 fun gcd x y = PolyML.IntInf.gcd (x, y);
 fun lcm x y = abs (PolyML.IntInf.lcm (x, y));
@@ -65,10 +52,3 @@
   | lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs));
 
 end;
-
-(* FIXME workaround for Poly/ML 5.7.1 testing *)
-structure IntInf =
-struct
-  open IntInf;
-  fun pow (i, n) = Integer.pow n i;
-end