Dear list,

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

Reply via email to