On 23/02/2016 19:05, Makarius wrote:
On Mon, 22 Feb 2016, David Matthews wrote:
There is a configure option --enable-intinf-as-int. This causes polyimport to build the basis library with int as arbitrary precision integer rather than fixed precision.
I have adapted to this change here: http://isabelle.in.tum.de/repos/isabelle/rev/ad3eb2889f9a
It works fine. I am rather glad that only some ML pretty printing required a different (approximative) int type.
I'm glad it's not too painful. I need to check more carefully that there aren't any other cases that really need to be fixed-precision but I think that's probably all.
One of the things I want to do as a result of removing arbitrary precision emulation is improve the way that long-form arbitrary precision values are handled. With emulation there is a sort of "cliff edge" where short-form values are handled very efficiently but long-form values that actually require emulating are considerably slower. Removing emulation should ultimately allow calls to C functions, such as the GMP library, to be speeded up.
David