[isabelle-dev] PolyML update

[Makarius]

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