[isabelle-dev] Integers in Poly/ML
makarius at sketis.net
Thu Nov 3 14:46:22 CET 2016
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
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 ...
More information about the isabelle-dev