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