The difference is substantial and uniform. I attach log files summarising MetiTarski’s performance by nearly 900 examples. You will note that total CPU time is way down, and problems consistently run much faster using fixed-precision arithmetic. Both runs involve the new version of Poly/ML, compiled with GMP.

Note that MetiTarski makes heavy use of large integers, hundreds or thousands of digits long, because of its use of rational numbers.

I actually can’t think of many places where Isabelle would need large integers, so it would probably benefit even more than MetiTarski does. 


On 2 Nov 2016, at 12:51, Makarius <> wrote:

I am surprised that MetiTarski shows such a relatively big speedup. Does
it really happen in a sustained manner for typical uses, and not just in
isolated cases?

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.

Attachment: STATUS-Metit-2016-10-11-60-test3-polyml.log
Description: Binary data

Attachment: STATUS-Metit-2016-10-31-60-fixed-int.log
Description: Binary data

isabelle-dev mailing list

Reply via email to