Incorrect result from signed right-shift when using Code_Target_Numeral
Makarius
makarius at sketis.net
Mon Dec 8 21:23:30 CET 2025
On 07/12/2025 00:03, Makarius wrote:
> The isabelle-release repository now has this changeset:
>
> changeset: 83717:f274b63c5b44
> tag: tip
> user: wenzelm
> date: Sat Dec 06 23:51:17 2025 +0100
> files: Admin/components/components.sha1 Admin/components/main
> description:
> update to polyml-5.9.2-2 version ccd3e3717f72 from branch fixes-5.9.2, which
> provides a corrected implementation of IntInf right shift;
> keep redundant checks for further testing;
>
>
> The plan is to publish it in Isabelle2025-1-RC4 next week (probably Monday),
> and remove the redundant check for the final release.
>
> The changeset will return to isabelle-dev shortly after Isabelle2025-1-RC4.
That is now isabelle-dev/c445b16fd5a9: it means that the state of affairs is
the same as for the final stage of the Isabelle2025-1 release process.
Makarius
More information about the isabelle-dev
mailing list