Re: [isabelle-dev] Failure in AFP when switching from polyml-5.6-1 to polyml-test-7a7b742897e9
On 08/12/16 17:41, David Matthews wrote: > > 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. This works, see http://isabelle.in.tum.de/repos/isabelle/rev/d23b7c9b9dd4 Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Failure in AFP when switching from polyml-5.6-1 to polyml-test-7a7b742897e9
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
