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.
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
In the meantime, David Matthews has revised many things, so it probably
works again, but it needs systematic testing on all platforms and
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.
isabelle-dev mailing list