[isabelle-dev] Integers in Poly/ML
Makarius
makarius at sketis.net
Sat Nov 5 22:28:26 CET 2016
On 02/11/16 13:51, Makarius wrote:
> On 02/11/16 13:07, Lawrence Paulson wrote:
>> David Matthews is working on a new release of Poly/ML in which the default type of integers is fixed-precision. A configuration option can restore the former set up, but that might be a mistake: I modified MetiTarski to use large integers only where needed and saw runtime decrease by around 30%. We could do the same. I imagine that we need large integers almost nowhere. Now consider that every bound variable is represented internally by an integer.
>
> I am surprised that MetiTarski shows such a relatively big speedup.
>
> My guess for Isabelle is between 0.1-5%, but it needs to be proven by
> concrete measurements. Changing type int to be a fixed-width machine
> word (and thus no int at all), will not work without significant work on
> the sources. Already about 10 years ago, we switched in the opposite
> direction, to make type int a proper integer even for SML/ML. That was a
> great improvement for tool development, and a slowdown for SML/NJ of
> 20-40% -- its IntInf implementation is very poor.
To conclude this thread properly, here are the results of a quick test
with ZF (spending only 20min on it). HOL probably requires much more
work to make it run, with its use of rational numbers etc.
Isabelle version: 2bf4fdcebd49
Poly/ML version: 55db4cc076ea8
ML_PLATFORM=x86_64-linux
ML_HOME="$HOME/lib/polyml/${ML_PLATFORM}"
ML_SYSTEM=polyml-5.6.1
ML_OPTIONS="-H 4000"
FixedInt:
isabelle build -g ZF -o threads=1
Finished Pure (0:00:19 elapsed time, 0:00:19 cpu time, factor 1.00)
Finished ZF (0:00:33 elapsed time, 0:00:33 cpu time, factor 1.00)
Finished ZF-AC (0:00:09 elapsed time, 0:00:09 cpu time, factor 1.00)
Finished ZF-Constructible (0:00:24 elapsed time, 0:00:24 cpu time,
factor 1.00)
Finished ZF-Induct (0:00:11 elapsed time, 0:00:11 cpu time, factor 1.00)
Finished ZF-UNITY (0:00:30 elapsed time, 0:00:30 cpu time, factor 1.00)
Finished ZF-ex (0:00:12 elapsed time, 0:00:12 cpu time, factor 1.00)
isabelle build -g ZF -o threads=4
Finished Pure (0:00:19 elapsed time, 0:00:19 cpu time, factor 1.00)
Finished ZF (0:00:16 elapsed time, 0:00:46 cpu time, factor 2.84)
Finished ZF-AC (0:00:04 elapsed time, 0:00:12 cpu time, factor 3.20)
Finished ZF-Constructible (0:00:12 elapsed time, 0:00:41 cpu time,
factor 3.18)
Finished ZF-Induct (0:00:05 elapsed time, 0:00:15 cpu time, factor 2.90)
Finished ZF-UNITY (0:00:11 elapsed time, 0:00:40 cpu time, factor 3.66)
Finished ZF-ex (0:00:07 elapsed time, 0:00:17 cpu time, factor 2.44)
IntInf:
isabelle build -g ZF -o threads=1
Finished Pure (0:00:22 elapsed time, 0:00:22 cpu time, factor 1.00)
Finished ZF (0:00:34 elapsed time, 0:00:34 cpu time, factor 1.00)
Finished ZF-AC (0:00:07 elapsed time, 0:00:07 cpu time, factor 1.00)
Finished ZF-Constructible (0:00:25 elapsed time, 0:00:25 cpu time,
factor 1.00)
Finished ZF-Induct (0:00:07 elapsed time, 0:00:07 cpu time, factor 1.00)
Finished ZF-UNITY (0:00:28 elapsed time, 0:00:28 cpu time, factor 1.00)
Finished ZF-ex (0:00:13 elapsed time, 0:00:13 cpu time, factor 1.00)
isabelle build -g ZF -o threads=4
Finished Pure (0:00:20 elapsed time, 0:00:20 cpu time, factor 1.00)
Finished ZF (0:00:18 elapsed time, 0:00:50 cpu time, factor 2.80)
Finished ZF-AC (0:00:03 elapsed time, 0:00:10 cpu time, factor 3.19)
Finished ZF-Constructible (0:00:10 elapsed time, 0:00:35 cpu time,
factor 3.20)
Finished ZF-Induct (0:00:03 elapsed time, 0:00:10 cpu time, factor 2.77)
Finished ZF-UNITY (0:00:11 elapsed time, 0:00:40 cpu time, factor 3.64)
Finished ZF-ex (0:00:07 elapsed time, 0:00:18 cpu time, factor 2.49)
This means there is no measurable difference, just some noise in the
data. So the actual speedup might be closer to 0.1% than to 5% in my
initial guess.
My original plan to experiment with FixedInt, when the Poly/ML
repository version is again fully working, had a much higher priority
before this mail thread. Now I will put it to the bottom of my TODO list.
There are so many better ways to scale Isabelle, by looking at the big
picture, instead of low-level tuning that degrades basic mathematical
concepts.
Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1478379718 -3600
# Sat Nov 05 22:01:58 2016 +0100
# Node ID b2ca5566c978c4b238c4126051a00fa6f60f64b2
# Parent 2bf4fdcebd495516947e5e85f3b3db01d5fbe1a4
test;
diff -r 2bf4fdcebd49 -r b2ca5566c978 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML Sat Nov 05 20:44:47 2016 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Sat Nov 05 22:01:58 2016 +0100
@@ -150,7 +150,7 @@
let
val (run, wait, wait_deps) =
(case timing of NONE => timing_start | SOME var => Synchronized.value var);
- fun micros time = string_of_int (Time.toNanoseconds time div 1000);
+ fun micros time = string_of_int (IntInf.toInt (Time.toNanoseconds time div 1000));
in
[("now", Value.print_real (Time.toReal (Time.now ()))),
("task_name", name), ("task_id", Value.print_int id),
diff -r 2bf4fdcebd49 -r b2ca5566c978 src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML Sat Nov 05 20:44:47 2016 +0100
+++ b/src/Pure/General/integer.ML Sat Nov 05 22:01:58 2016 +0100
@@ -36,7 +36,7 @@
fun sign x = int_ord (x, 0);
-fun div_mod x y = IntInf.divMod (x, y);
+fun div_mod x y = apply2 IntInf.toInt (IntInf.divMod (IntInf.fromInt x, IntInf.fromInt y));
fun square x = x * x;
@@ -55,13 +55,13 @@
else pw k l
end;
-fun gcd x y = PolyML.IntInf.gcd (x, y);
-fun lcm x y = abs (PolyML.IntInf.lcm (x, y));
+fun gcd x y = IntInf.toInt (PolyML.IntInf.gcd (IntInf.fromInt x, IntInf.fromInt y));
+fun lcm x y = abs (IntInf.toInt (PolyML.IntInf.lcm (IntInf.fromInt x, IntInf.fromInt y)));
fun gcds [] = 0
| gcds (x :: xs) = fold gcd xs x;
fun lcms [] = 1
- | lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs));
+ | lcms (x :: xs) = abs (Library.foldl (uncurry lcm) (x, xs));
end;
diff -r 2bf4fdcebd49 -r b2ca5566c978 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML Sat Nov 05 20:44:47 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML Sat Nov 05 22:01:58 2016 +0100
@@ -105,8 +105,8 @@
fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
| reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
- | reported loc (PolyML.PTdefId id) = reported_entity_id true (FixedInt.toLarge id) loc
- | reported loc (PolyML.PTrefId id) = reported_entity_id false (FixedInt.toLarge id) loc
+ | reported loc (PolyML.PTdefId id) = reported_entity_id true id loc
+ | reported loc (PolyML.PTrefId id) = reported_entity_id false id loc
| reported loc (PolyML.PTtype types) = reported_types loc types
| reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
| reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
More information about the isabelle-dev
mailing list