Re: [isabelle-dev] Failure in AFP when switching from polyml-5.6-1 to polyml-test-7a7b742897e9

2016-12-08 Thread David Matthews


On 08/12/2016 15:01, Florian Haftmann wrote:

Hi all,

when testing polyml-test-7a7b742897e9 I found out that this breaks
session Algebraic_Numbers in the AFP:

*** At command "value" (line 42 of
"/mnt/home/haftmann/data/tum/afp/devel/thys/Algebraic_Numbers/Algebraic_Number_Tests.thy")
*** exception Div raised (line 302 of "./basis/InitialBasis.ML")

It looks like a change in the semantics of integer division in PolyML,
but this is entirely speculative.



No, it was a bug in the testing version of Poly/ML.  Thanks for pointing 
it out and in particular including the line number which allowed me to 
see immediately what was wrong.  Hopefully the commit I've just pushed 
will have fixed it.


David

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


[isabelle-dev] Failure in AFP when switching from polyml-5.6-1 to polyml-test-7a7b742897e9

2016-12-08 Thread Florian Haftmann
Hi all,

when testing polyml-test-7a7b742897e9 I found out that this breaks
session Algebraic_Numbers in the AFP:

*** At command "value" (line 42 of
"/mnt/home/haftmann/data/tum/afp/devel/thys/Algebraic_Numbers/Algebraic_Number_Tests.thy")
*** exception Div raised (line 302 of "./basis/InitialBasis.ML")

It looks like a change in the semantics of integer division in PolyML,
but this is entirely speculative.

The corresponding HG ids are near
Isabelle: 3d4331b65861
AFP:  74c0b7f55fa2

Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev