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

[Makarius]

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