[isabelle-dev] PolyML update
andreas.lochbihler at inf.ethz.ch
Fri Aug 11 18:31:14 CEST 2017
I've been playing around with adding unsigned 64 bit integers to the AFP entry
Native_Word. In doing so, 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. The problem seems to be fixed in PolyML 5.7. I am now hesitant to
update my AFP entry because (1) I cannot include all the test cases for Uint64 that I want
and (2) if PolyML 5.6-1 is also shipped with the next release, then users might prove
False by exploiting this error.
Are there any plans to update to PolyML 5.7 before the release?
More information about the isabelle-dev