[isabelle-dev] Isabelle2024-RC0: Issue with LargeInt.int <> int unification

[Joshua K.]

Hi,

The PolyML version, 5.9.1, bundled with the Isabelle 2024 rc0 currently fails to build Pure on my system. The error stems from polyml getting stuck at unifying LargeInt.int and int. Is this an expected behavior?

This specifically occurs[^0] in Pure/ML/ml_statistics.ML where make_properties received multiple LargeInt.int values from SizeStat Statistics, like, e.g., sizeAllocation. The unification would then be required when this value is passed to print_int which tries to apply Int.toString. I've attached a build log with the full error message.

This specific instance can be quickly resolved by making a specialized print_int for LargeInt values. An example of such a change is attached as a small patch. However, even after this patch there are still other instances of the same error throughout the Pure codebase, e.g., in Pure/General/integer.ML.

Best regards,

Joshua Kobschätzki

-----------------------------------
Joshua Kobschätzki
w: https://cobalt.rocks
e: joshua.kobschaetzki at cobalt.rocks
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240312/df79ea87/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Pure.log
Type: text/x-log
Size: 3920 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240312/df79ea87/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: isabelle-polyml-api.patch
Type: text/x-patch
Size: 1556 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240312/df79ea87/attachment-0001.bin>