If there is really such a serious bug, we should update asap, imho<br><br>Peter<div class="quote" style="line-height: 1.5"><br><br>-------- Original Message --------<br>Subject: [isabelle-dev] PolyML update<br>From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch><br>To: DEV Isabelle Mailinglist <isabelle-dev@in.tum.de><br>CC: <br><br><br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear list,<br><br>I've been playing around with adding unsigned 64 bit integers to the AFP entry <br>Native_Word. In doing so, I realised that PolyML in 64 bit mode has a bug in the Word64 <br>implementation in the version that the current development version 2a6371fb31f0 uses <br>(PolyML 5.6-1). For example, dividing 18446744073709551611 by 3 using the Word64 structure <br>gives a wrong result. The problem seems to be fixed in PolyML 5.7. I am now hesitant to <br>update my AFP entry because (1) I cannot include all the test cases for Uint64 that I want <br>and (2) if PolyML 5.6-1 is also shipped with the next release, then users might prove <br>False by exploiting this error.<br><br>Are there any plans to update to PolyML 5.7 before the release?<br><br>Andreas<br>_______________________________________________<br>isabelle-dev mailing list<br>isabelle-dev@in.tum.de<br>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br></blockquote></div>