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

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

Reply via email to