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



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.

After a bit more use, I noticed another strange pattern. Poly/ML accumulates heap very quickly, but if I manually run

  PIDE.session.protocol_command("ML_Heap.full_gc")

in the Console dockable, thus forcing a GC run, it completes within a few seconds (as expected).

Curiously enough, when an automatic GC run happens, Poly/ML does not appear to release memory back to the OS, but running the above command does.

--
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.