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