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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev