[isabelle-dev] Integers in Poly/ML

[Makarius]

On 03/11/16 13:47, Lawrence Paulson wrote:
> Just as remark: MetiTarski took a slight performance hit in the
> transition to the new compiler, happily greatly reversed by my decision
> to use fixed-precision integers.

That taken alone would have meant a step backwards: proper integers have
become non-integers, just to follow the errors of the majority in the
last decades.

Luckily the situation is not as bad, and David Matthews continues to
consolidate the new compiler and run-time system: Isabelle is already a
bit faster than before, while still remaining true to mathematical
semantics of int.

More tuning and measurements will follow in the coming weeks/months ...


	Makarius