[isabelle-dev] PolyML update
makarius at sketis.net
Fri Aug 11 22:59:34 CEST 2017
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.
More information about the isabelle-dev