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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
