Incorrect result from signed right-shift when using Code_Target_Numeral

Makarius makarius at sketis.net
Fri Dec 5 14:44:20 CET 2025


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. *)


	Makarius



More information about the isabelle-dev mailing list