Hi Makarius and Peter, I agree that the Word64 structure is, at least for regular Isabelle usage, so far essentially dead code. PolyML only supports it in 64-bit mode, so essentially no Isabelle application should be using it so far. It's also probably unused for SMLNJ because of the inefficiency of its implementation. For PolyML and mlton, I would not be so sure about whether IntInf.int is faster than Word64. IIRC David Matthews reworked the implementation of Word64 for PolyML 5.7 and mlton has primitive operation implementations for Word64. One would have to do a few measurements to really say.
So, the PolyML-5.6 flaws in the implementation of Word64 are not mission critical for Isabelle and there is no urgent need to update PolyML just because of this. But in general, especially for other code generator languages like Scala, 64 bit arithmetic is definitely faster than unbounded integer arithmetic. And this is what Native_Word is good for. Andreas ________________________________________ Von: Makarius [makar...@sketis.net] Gesendet: Freitag, 11. August 2017 22:59 An: Lochbihler Andreas; DEV Isabelle Mailinglist Betreff: Re: [isabelle-dev] PolyML update 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
