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