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