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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
