Re: [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 <makar...@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.

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

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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev