Re: [isabelle] Isabelle2021-1-RC3: excessive Poly/ML heap requirements



On 23/11/2021 15:45, Lars Hupel wrote:
> 
> I'm porting a small but substantial application (~ 7kLOC, but no custom
> tactics or commands) to Isabelle2021-1.
> 
> I noticed during regular development with Isabelle/jEdit that Poly/ML quite
> aggressively allocates memory. I have a quad-core machine with 24 GB of
> memory, and it is not uncommon for me to see heap sizes > 10 GB.

What is your OS version?

Can you can try this with other versions of Poly/ML? Here are some formal
component names:

#bundled with Isabelle2021
polyml-test-f86ae3dc1686

#official release after Isabelle2021
polyml-5.8.2

#approximations of polyml-5.9 for Isabelle2021-1
polyml-5.9-960de0cd0795
polyml-5.9-5d4caa8f7148
polyml-5.9-cc80e2b43c38
polyml-5.9-610a153b941d


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.