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

[Makarius]

On 03/11/17 19:26, Fabian Immler wrote:
> I looked at it once more: profiling told me that IntInf.pow (in combination with Par_List.map) seems to be the culprit.
> 
> The following snippet shows similar behavior:
> ML ‹
> fun powers [] = []
>  | powers (x::xs) = IntInf.pow (2, x mod 15)::powers xs;
> Par_List.map (fn i => powers (i upto 100000 * i)) (0 upto 31)
> ›
> 
> polyml-5.6-1/x86_64-linux: 0:00:08 elapsed time, 0:00:35 cpu time, factor 4.02
> polyml-test-e8d82343b692/x86_64-linux: 0:00:36 elapsed time, 0:03:26 cpu time, factor 5.70
> polyml-5.6-1/x86_64-darwin:  0.570s elapsed time, 1.748s cpu time, 0.000s GC time
> polyml-test-e8d82343b692/x86_64-darwin: 522.080s elapsed time, 568.676s cpu time, 42.602s GC time

I have discovered the same and have now pushed a workaround:
http://isabelle.in.tum.de/repos/isabelle/rev/17eb23e43630

Somehow the IntInf.pow implementation in Poly/ML e8d82343b692 is a bit
wasteful, maybe during the bit vector operation instead of our
IntInf.divMod (_, 2) used here: see
http://isabelle.in.tum.de/repos/isabelle/annotate/17eb23e43630/src/Pure/General/integer.ML#l43

With that little change, I get the following very good timings on lxcisa0:

  ML_PLATFORM="x86_64-linux"
  ML_HOME="/home/isabelle/contrib/polyml-test-e8d82343b692/x86_64-linux"
  ML_SYSTEM="polyml-5.7.1"
  ML_OPTIONS="--minheap 4G --maxheap 32G"

$ 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


	Makarius