Peter
-------- Original Message --------
Subject: [isabelle-dev] PolyML update
From: Andreas Lochbihler
To: DEV Isabelle Mailinglist
CC:
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?
Andreas
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
