On 11/08/17 22:59, Makarius wrote:
>
> Poly/ML 5.7 does not work for Isabelle
>
> 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 made some experiments with the Poly/ML rep
than unbounded integer
arithmetic. And this is what Native_Word is good for.
Andreas
Von: Makarius [makar...@sketis.net]
Gesendet: Freitag, 11. August 2017 22:59
An: Lochbihler Andreas; DEV Isabelle Mailinglist
Betreff: Re: [isabelle-dev] PolyML update
On
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
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_Wor
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, di