Email Gateway (Mar 12 2024 at 16:32): Email Gateway (Mar 12 2024 at 16:32):From: "Joshua K." <j.kobschaetzki@campus.tu-berlin.de>
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@cobalt.rocks
Pure.log
isabelle-polyml-api.patch
Email Gateway (Mar 12 2024 at 16:44):From: Makarius <makarius@sketis.net>
I am unsure what you mean. Poly/ML needs to be built with specific options, in
order to work with Isabelle: the result is provided as Isabelle component.
In that environment, type int is always unbounded mathematical int, as always
in the past 3 decades.
Are you actually using the downloads from
https://isabelle.in.tum.de/website-Isabelle2024-RC0 or something else?
Alternatively, you can build from the repository, following README_REPOSITORY.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 28 2024 at 12:28 UTC