Re: [isabelle-dev] PolyML update

2017-08-11 Thread Makarius 
On 11/08/17 18:31, Andreas Lochbihler wrote:
> 
> 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.

I guess that Word64 has been de-facto dead code of the SML basis library
for many years: I've never seen any Isabelle application using it. It is
also less efficient than proper (unbounded) integers, due to extra
boxing required for fixed-size 64bit entities.


> Are there any plans to update to PolyML 5.7 before the release?

Poly/ML 5.7 does not work for Isabelle, as already pointed out in this
thread
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg07353.html
from 15-May-2017.

In the meantime, David Matthews has revised many things, so it probably
works again, but it needs systematic testing on all platforms and
32/64bit combinations.

I have presently no idea about release plans of Poly/ML 5.7.x. Anything
for Isabelle2017 needs to happen within the next 4-6 weeks.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] PolyML update

2017-08-11 Thread Peter Lammich 
If there is really such a serious bug, we should update asap, imhoPeter Original Message Subject: [isabelle-dev] PolyML updateFrom: 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 listisabelle-...@in.tum.dehttps://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

[isabelle-dev] PolyML update

2017-08-11 Thread Andreas Lochbihler 

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