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?
isabelle-dev mailing list