Incorrect result from signed right-shift when using Code_Target_Numeral
Makarius
makarius at sketis.net
Fri Dec 5 13:34:16 CET 2025
On 05/12/2025 01:43, Daniel Matichuk via isabelle-dev wrote:
>
> After some investigation I've determined that this is an issue that was
> introduced in PolyML 5.6.2, which I've reported here:
>
> 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.
For now, lets hope that David Matthews will do something on the spot --- I've
added some further bits of information to the above ticket.
Makarius
More information about the isabelle-dev
mailing list