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

Dear list,

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.

Normally, that wouldn't be a problem, however the GC/ML cleanup can take a long time, during which my entire laptop freezes (unless the OOM killer chimes in). Just now I saw a GC phase that took ~50 seconds with an ML heap size of 2 GB.


Lars Hupel, lars.hupel at innoq.com, https://www.innoq.com
innoQ Deutschland GmbH, Krischerstr. 100, 40789 Monheim am Rhein, Germany

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