Incorrect result from signed right-shift when using Code_Target_Numeral

[Daniel Matichuk]

I tried to test the updated polyml version, but ran into an issue with
component_polyml:

./bin/isabelle component_polyml -V 64eb08b0a4bcb20d39167550034f30d05a61f121
Creating component directory
"/Users/dmatichuk/Code/isabelle/polyml-64eb08b0a4bcb20d39167550034f30d05a61f121"
Getting "https://gmplib.org/download/gmp/gmp-6.3.0.tar.bz2"
Building GMP library ...
Getting "
https://github.com/polyml/polyml/archive/64eb08b0a4bcb20d39167550034f30d05a61f121.tar.gz
"
Getting "https://files.sketis.net/sha1/archive/0ce12663fe76.tar.gz"
Building Poly/ML arm64_32-darwin
*** error: /Library/Developer/CommandLineTools/usr/bin/install_name_tool:
more than one input file specified (poly and poly)
*** Usage: /Library/Developer/CommandLineTools/usr/bin/install_name_tool
[-change old new] ... [-rpath old new] ... [-add_rpath new] ...
[-delete_rpath old] ... [-id name] input

A quick fix was to simply modify executable.scala/library_closure to
instead call install_name_tool multiple times.



On Fri, Dec 5, 2025 at 5:44 AM 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. *)
>
>
>         Makarius
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251205/b5744d68/attachment-0001.htm>