On 12/03/2024 17:30, Joshua K. wrote:
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?
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-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
