
<!DOCTYPE html><html><body><div dir="auto">Hi,<br><br>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?<br><br>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.<br><br>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.<br><br>Best regards,<br><br>Joshua Kobschätzki<br></div><div dir="auto"><hr>Joshua Kobschätzki<br>w: <a href="https://cobalt.rocks">https://cobalt.rocks</a><br>e: joshua.kobschaetzki@cobalt.rocks</div></body></html>