On 11/08/17 18:31, Andreas Lochbihler wrote: > > I realised that PolyML in 64 bit mode > has a bug in the Word64 implementation in the version that the current > development version 2a6371fb31f0 uses (PolyML 5.6-1). For example, > dividing 18446744073709551611 by 3 using the Word64 structure gives a > wrong result.
I guess that Word64 has been de-facto dead code of the SML basis library for many years: I've never seen any Isabelle application using it. It is also less efficient than proper (unbounded) integers, due to extra boxing required for fixed-size 64bit entities. > Are there any plans to update to PolyML 5.7 before the release? Poly/ML 5.7 does not work for Isabelle, as already pointed out in this thread http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg07353.html from 15-May-2017. In the meantime, David Matthews has revised many things, so it probably works again, but it needs systematic testing on all platforms and 32/64bit combinations. I have presently no idea about release plans of Poly/ML 5.7.x. Anything for Isabelle2017 needs to happen within the next 4-6 weeks. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev