<!DOCTYPE html>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<div class="moz-cite-prefix">Hi,</div>
<div class="moz-cite-prefix">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". </div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">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:</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">ML\<open></div>
<div class="moz-cite-prefix"> PackReal32Little.fromBytes
(Word8Vector.fromList [0wxC5, 0wx10, 0wxE8, 0wx3B])</div>
<div class="moz-cite-prefix">\<close></div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">returns a different value, namely:</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">* Isabelle 2025:
val it = 0.007082077209: PackReal32Little.real</div>
<div class="moz-cite-prefix">* Isabelle development/2025-1: val
it = 0.007082077: PackReal32Little.real</div>
<div class="moz-cite-prefix"><br>
</div>
<p>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. </p>
<p>We will take care of this tomorrow. </p>
<p><br>
</p>
<p>Best,</p>
<p>Achim (and Amy) </p>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">On 19/11/2025 16:25, Lawrence Paulson
via isabelle-dev wrote:<br>
</div>
<blockquote type="cite"
cite="mid:8c21d775-80da-4d58-82d5-6f77ab9e67d1@Spark">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title></title>
<div name="messageBodySection">
<div dir="auto">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.</div>
</div>
<div name="messageSignatureSection"><br>
<div class="matchFont">Larry</div>
</div>
</blockquote>
<p><br>
</p>
</body>
</html>