Stream: Mirror: Isabelle Development Mailing List

Topic: Incorrect result from signed right-shift when using Code_...

view this post on Zulip Email Gateway (Dec 05 2025 at 00:44):

From: Daniel Matichuk via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>

In Isabelle-2025-RC1 the following theory yields an incorrect result from
"value" (Hex_Words is optional):

theory "Scratch"
imports "HOL-Library.Word" "HOL-Library.Code_Target_Numeral"
"Word_Lib.Hex_Words"
begin

value "signed_drop_bit 5 ((0x80000010 :: 32 word))"
(* "0xFC000001" :: "32 word" *)

end

However the correct result (0xFC000000) is given if Code_Target_Numeral is
not imported.

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

view this post on Zulip Email Gateway (Dec 05 2025 at 12:34):

From: Makarius <makarius@sketis.net>

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

view this post on Zulip Email Gateway (Dec 05 2025 at 13:45):

From: Makarius <makarius@sketis.net>

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

view this post on Zulip Email Gateway (Dec 05 2025 at 21:34):

From: Daniel Matichuk via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>

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@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

view this post on Zulip Email Gateway (Dec 05 2025 at 21:42):

From: Makarius <makarius@sketis.net>

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

view this post on Zulip Email Gateway (Dec 05 2025 at 21:59):

From: Makarius <makarius@sketis.net>

On 05/12/2025 22:42, Makarius wrote:

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.

I now see 638379c583a5, and that looks fine so far in a quick test of
HOL-Codegenerator_Test ...

Makarius

view this post on Zulip Email Gateway (Dec 05 2025 at 22:18):

From: Daniel Matichuk via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>

Some quick tests with the code generator indicate that this revision seems
to have resolved the issue (compiled with GMP enabled, using arm64_32).

On Fri, Dec 5, 2025 at 1:58 PM Makarius <makarius@sketis.net> wrote:

On 05/12/2025 22:42, Makarius wrote:

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.

I now see 638379c583a5, and that looks fine so far in a quick test of
HOL-Codegenerator_Test ...

Makarius

view this post on Zulip Email Gateway (Dec 06 2025 at 07:32):

From: Peter Lammich <lammich@in.tum.de>

We have to disable code generator setup that could cause by eval to
malfunction, when this buggy polyml makes it into the release. And check that
Isabelle itself doesn't rely on the shift operation 

On 5 Dec 2025 14:44, Makarius <makarius@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

view this post on Zulip Email Gateway (Dec 06 2025 at 12:13):

From: Makarius <makarius@sketis.net>

On 5 Dec 2025 14:44, Makarius <makarius@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. *)

On 05/12/2025 18:20, Peter Lammich wrote:

We have to disable code generator setup that could cause by eval to
malfunction, when this buggy polyml makes it into the release. And check that
Isabelle itself doesn't rely on the shift operation

It is clear that this version will not be in the final release. There will
already be a different polyml setup for Isabelle2025-1-RC4, published next week.

Makarius

view this post on Zulip Email Gateway (Dec 06 2025 at 15:45):

From: Florian Haftmann <florian.haftmann@cit.tum.de>

Am 05.12.25 um 22:58 schrieb Makarius:

On 05/12/2025 22:42, Makarius wrote:

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.

I now see 638379c583a5, and that looks fine so far in a quick test of
HOL-Codegenerator_Test ...

It is interesting that this remained undiscovered – AFP session
Native_Word contains considerable tests for code generation for word types.

I’ll investigate what is missing there.

Cheers,
Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

view this post on Zulip Email Gateway (Dec 06 2025 at 23:01):

From: Makarius <makarius@sketis.net>

On 06/12/2025 16:44, Florian Haftmann wrote:

It is interesting that this remained undiscovered – AFP session Native_Word
contains considerable tests for code generation for word types.

I’ll investigate what is missing there.

Maybe this version on isabelle-release helps:

changeset: 83716:4885450ab48d
tag: tip
user: wenzelm
date: Sat Dec 06 23:01:40 2025 +0100
files: src/Pure/ML/ml_init.ML
description:
expose bad IntInf shift operations in Poly/ML via explicit exceptions;

Testing it with afp-2025-1/3af26ffddf1b (-X slow) does not expose any errors,
though.

Makarius

view this post on Zulip Email Gateway (Dec 06 2025 at 23:03):

From: Makarius <makarius@sketis.net>

The isabelle-release repository now has this changeset:

changeset: 83717:f274b63c5b44
tag: tip
user: wenzelm
date: Sat Dec 06 23:51:17 2025 +0100
files: Admin/components/components.sha1 Admin/components/main
description:
update to polyml-5.9.2-2 version ccd3e3717f72 from branch fixes-5.9.2, which
provides a corrected implementation of IntInf right shift;
keep redundant checks for further testing;

The plan is to publish it in Isabelle2025-1-RC4 next week (probably Monday),
and remove the redundant check for the final release.

The changeset will return to isabelle-dev shortly after Isabelle2025-1-RC4.

Makarius

view this post on Zulip Email Gateway (Dec 08 2025 at 20:24):

From: Makarius <makarius@sketis.net>

On 07/12/2025 00:03, Makarius wrote:

The isabelle-release repository now has this changeset:

changeset:   83717:f274b63c5b44
tag:         tip
user:        wenzelm
date:        Sat Dec 06 23:51:17 2025 +0100
files:       Admin/components/components.sha1 Admin/components/main
description:
update to polyml-5.9.2-2 version ccd3e3717f72 from branch fixes-5.9.2, which
provides a corrected implementation of IntInf right shift;
keep redundant checks for further testing;

The plan is to publish it in Isabelle2025-1-RC4 next week (probably Monday),
and remove the redundant check for the final release.

The changeset will return to isabelle-dev shortly after Isabelle2025-1-RC4.

That is now isabelle-dev/c445b16fd5a9: it means that the state of affairs is
the same as for the final stage of the Isabelle2025-1 release process.

Makarius

Last updated: Dec 10 2025 at 12:50 UTC