[isabelle-dev] Integers in Poly/ML

[Lawrence Paulson]

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. 

Larry

> On 2 Nov 2016, at 12:51, Makarius <makarius at sketis.net> 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.
> 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161102/ae15d21b/attachment-0006.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: STATUS-Metit-2016-10-11-60-test3-polyml.log
Type: application/octet-stream
Size: 39589 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161102/ae15d21b/attachment-0004.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161102/ae15d21b/attachment-0007.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: STATUS-Metit-2016-10-31-60-fixed-int.log
Type: application/octet-stream
Size: 39563 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161102/ae15d21b/attachment-0005.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161102/ae15d21b/attachment-0008.html>