[isabelle-dev] PolyML update

[Lochbihler Andreas]

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 [makarius at 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