Re: [isabelle-dev] PolyML update

[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 repository version
938336aeb7eb from 02-Aug-2017, but it does not quite work (problem with
HOL-Decision_Procs).

David Matthews is in the middle of substantial changes again, so this is
probably to be expected.


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

Re: [isabelle-dev] PolyML update

[Lochbihler Andreas]

Hi Makarius and Peter,

I agree that the Word64 structure is, at least for regular Isabelle usage, so 
far essentially dead code. PolyML only supports it in 64-bit mode, so 
essentially no Isabelle application should be using it so far. It's also 
probably unused for SMLNJ because of the inefficiency of its implementation. 
For PolyML and mlton, I would not be so sure about whether IntInf.int is faster 
than Word64. IIRC David Matthews reworked the implementation of Word64 for 
PolyML 5.7 and mlton has primitive operation implementations for Word64. One 
would have to do a few measurements to really say.

So, the PolyML-5.6 flaws in the implementation of Word64 are not mission 
critical for Isabelle and there is no urgent need to update PolyML just because 
of this. But in general, especially for other code generator languages like 
Scala, 64 bit arithmetic is definitely faster 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 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

[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

[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