Email Gateway (Nov 20 2025 at 12:14): Email Gateway (Nov 20 2025 at 12:14):From: Peter Lammich <lammich@in.tum.de>
It looks like what has changed is the pretty-printing. I think (just did
a quick check with Java) as a IEEE-32 value, both numbers are the same
(the closest IEEE-32 floating point number to this decimal
representation is the same, namely 3be810c5).
--
Peter
On 20/11/2025 12:35, Lawrence Paulson wrote:
I find it surprising that the meaning of a specific bit pattern as a real number according to an established floating-point standard can change from year to year. How do we know it won't change again?
Larry
On 19 Nov 2025, at 22:37, Achim D. Brucker <adbrucker@0x5f.org> wrote:
Hi,
I did a first investigation. Overall, this part of the theory is intended to serve as regression test. Thus, it worked as it should: acting as early warning for subtle changes that otherwise would go undetected, potentially creating "bit rot".The change is actually due to a difference in Poly/ML used in Isabelle 2025 vs the current development version (and, 2025-1, for that matter). Namely:
ML\<open>
PackReal32Little.fromBytes (Word8Vector.fromList [0wxC5, 0wx10, 0wxE8, 0wx3B])
\<close>returns a different value, namely:
- Isabelle 2025: val it = 0.007082077209: PackReal32Little.real
- Isabelle development/2025-1: val it = 0.007082077: PackReal32Little.real
As the rule-of-thumb regarding the precision of 32 IEEE-745 floating point numbers is around 7-8 decimal digits, the new behaviour is OK. Hence, the fix to get the AFP entry working again is to update the theories to reflect the new values.
We will take care of this tomorrow.Best,
Achim (and Amy)On 19/11/2025 16:25, Lawrence Paulson via isabelle-dev wrote:
Neural_Networks is badly broken. I took a look and the failure is in a proof that tests whether a certain generated construction is equal to an explicit construction. They are supposed to be literally identical and are not. I think we should get back to the authors to find out why it failed and how it can be made robust.
Larry
Afp-submit mailing list
Afp-submit@mailman.proof.cit.tum.de
https://mailman46.in.tum.de/mailman/listinfo/afp-submit
Email Gateway (Nov 20 2025 at 13:21):From: "Achim D. Brucker" <adbrucker@0x5f.org>
Hi,
This is also my assumption. The values used by me in the below example
are after pretty printing (i.e., convertio to strings).
The actually value stored is 0.070820772089064121246337890625 (decoding
it "manually", following the standard). Trying to print it in a small C
programm gives 0.00708207720890641212, which seems to be the offical
decimal represenation according to the standard. IEEE754 is not easy ...
Achim
On 20/11/2025 12:14, Peter Lammich wrote:
It looks like what has changed is the pretty-printing. I think (just
did a quick check with Java) as a IEEE-32 value, both numbers are the
same (the closest IEEE-32 floating point number to this decimal
representation is the same, namely 3be810c5).--
Peter
On 20/11/2025 12:35, Lawrence Paulson wrote:
I find it surprising that the meaning of a specific bit pattern as a
real number according to an established floating-point standard can
change from year to year. How do we know it won't change again?Larry
On 19 Nov 2025, at 22:37, Achim D. Brucker <adbrucker@0x5f.org> wrote:
Hi,
I did a first investigation. Overall, this part of the theory is
intended to serve as regression test. Thus, it worked as it should:
acting as early warning for subtle changes that otherwise would go
undetected, potentially creating "bit rot".The change is actually due to a difference in Poly/ML used in
Isabelle 2025 vs the current development version (and, 2025-1, for
that matter). Namely:ML\<open>
PackReal32Little.fromBytes (Word8Vector.fromList [0wxC5, 0wx10,
0wxE8, 0wx3B])
\<close>returns a different value, namely:
- Isabelle 2025: val it =
0.007082077209: PackReal32Little.real- Isabelle development/2025-1: val it = 0.007082077:
PackReal32Little.realAs the rule-of-thumb regarding the precision of 32 IEEE-745 floating
point numbers is around 7-8 decimal digits, the new behaviour is OK.
Hence, the fix to get the AFP entry working again is to update the
theories to reflect the new values.
We will take care of this tomorrow.Best,
Achim (and Amy)On 19/11/2025 16:25, Lawrence Paulson via isabelle-dev wrote:
Neural_Networks is badly broken. I took a look and the failure is
in a proof that tests whether a certain generated construction is
equal to an explicit construction. They are supposed to be
literally identical and are not. I think we should get back to the
authors to find out why it failed and how it can be made robust.Larry
Afp-submit mailing list
Afp-submit@mailman.proof.cit.tum.de
https://mailman46.in.tum.de/mailman/listinfo/afp-submit
Email Gateway (Nov 20 2025 at 14:21):From: Makarius <makarius@sketis.net>
On 20/11/2025 14:21, Achim D. Brucker wrote:
The actually value stored is 0.070820772089064121246337890625 (decoding it
"manually", following the standard). Trying to print it in a small C programm
gives 0.00708207720890641212, which seems to be the offical decimal
represenation according to the standard. IEEE754 is not easy ...
Note that there have been changes on reals in polyml-5.9.1 (Isabelle2025) to
polyml-5.9.2 (Isabelle2025-1).
An example changeset by David Matthews is here
https://github.com/polyml/polyml/commit/cc497eb585b0
Maybe someone who understands the fine points can check if it has become more
correct or less correct.
Makarius
Email Gateway (Nov 20 2025 at 14:41):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
I know that converting a floating point number to decimal notation is tricky, but we must've had correct algorithms for decades now. I wonder whether anybody has formalised one :-)
Larry
On 20 Nov 2025 at 13:21 +0000, Achim D. Brucker <adbrucker@0x5f.org>, wrote:
This is also my assumption. The values used by me in the below example
are after pretty printing (i.e., convertio to strings).
The actually value stored is 0.070820772089064121246337890625 (decoding
it "manually", following the standard). Trying to print it in a small C
programm gives 0.00708207720890641212, which seems to be the offical
decimal represenation according to the standard. IEEE754 is not easy ...
Email Gateway (Nov 20 2025 at 15:28):From: Peter Lammich <lammich@in.tum.de>
I remember having seen a talk about that ... but I cannot find any
matching papers :(
On 20/11/2025 15:40, Lawrence Paulson wrote:
I know that converting a floating point number to decimal notation is
tricky, but we must've had correct algorithms for decades now. I
wonder whether anybody has formalised one :-)Larry
On 20 Nov 2025 at 13:21 +0000, Achim D. Brucker <adbrucker@0x5f.org>,
wrote:This is also my assumption. The values used by me in the below example
are after pretty printing (i.e., convertio to strings).The actually value stored is 0.070820772089064121246337890625 (decoding
it "manually", following the standard). Trying to print it in a small C
programm gives 0.00708207720890641212, which seems to be the offical
decimal represenation according to the standard. IEEE754 is not easy ...
Last updated: Dec 10 2025 at 12:50 UTC