Re: [isabelle-dev] PolyML update

2017-08-13 Thread Makarius
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

Re: [isabelle-dev] PolyML update

2017-08-12 Thread Lochbihler Andreas
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 11/08

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

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