Incorrect result from signed right-shift when using Code_Target_Numeral

[Makarius]

On 05/12/2025 22:33, Daniel Matichuk wrote:
> 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"

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

That is a conflict of a locally installed libgmp with the one that is built 
via "isabelle component_polyml". The usual workaround is to remove that other 
libgmp, which is usually in /usr/local.

That is indeed a bit awkward, but "isabelle component_polyml" is merely an 
administrative tool for limited contexts. I usually need several attempts to 
make it work with "current" OS versions, whatever they are.

Right now our main problem is that 64eb08b0a4bc is on top of "latest" Poly/ML 
development and experiments. Thus it does not quite work for Isabelle yet, 
especially HOL-Codegenerator_Test. For the release the change needs to sit on 
top of official v5.9.2.


	Makarius