Incorrect result from signed right-shift when using Code_Target_Numeral

[Makarius]

 > On 5 Dec 2025 14:44, Makarius <makarius at sketis.net> wrote:
 >
 >     On 05/12/2025 13:34, Makarius wrote:
 >      >>
 >      >> https://github.com/polyml/polyml/issues/243 <https://github.com/polyml/
 >      >> polyml/ issues/243>
 >      >
 >      > Thanks for the report. It is very relevant for the Isabelle2025-1
 >     release: in
 >      > the worst case we need to switch back to Poly/ML 5.9.1, see also
 >      > Isabelle/08722f90a439.
 >
 >     The worst case is probably not that bad: it should be sufficient to revert
 >     this change: https://github.com/polyml/polyml/commit/ed1ff06d7b53
 >
 >     There is also an interesting comment in the old version:
 >
 >         (* These could be implemented in the RTS although I doubt if it's
 >            really worth it. *)

On 05/12/2025 18:20, Peter Lammich wrote:
> We have to disable code generator setup that could cause by eval to 
> malfunction, when this buggy polyml makes it into the release. And check that 
> Isabelle itself doesn't rely on the shift operation

It is clear that this version will not be in the final release. There will 
already be a different polyml setup for Isabelle2025-1-RC4, published next week.


	Makarius