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_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,
Building HOL-ODE-Numerics ...
Finished HOL-ODE-Numerics (0:18:23 elapsed time, 0:43:51 cpu time,
Building Lorenz_Approximation ...
Finished Lorenz_Approximation (0:03:51 elapsed time, 0:08:15 cpu time,
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
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
> 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
# HG changeset patch
# User wenzelm
# Date 1509824436 -3600
# Sat Nov 04 20:40:36 2017 +0100
# Node ID 415a6bba9344b53576477a6e03d6ea5f6219ad1d
# Parent 978c584609ded0d1a36246b83aeb8630d14034f9
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 =
- fun pw 0 _ = 1
- | pw 1 l = l
- | pw k l =
- val (k', r) = div_mod k 2;
- val l' = pw k' (l * l);
- in if r = 0 then l' else l' * l end;
- if k < 0
- then IntInf.pow (l, k)
- else pw k l
+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));
-(* FIXME workaround for Poly/ML 5.7.1 testing *)
-structure IntInf =
- open IntInf;
- fun pow (i, n) = Integer.pow n i;
isabelle-dev mailing list