Stream: General

Topic: frequent GC when memory is sufficient


view this post on Zulip Qiyuan Xu (Aug 26 2022 at 09:02):

Hi guys, I noticed my Isabelle recently does GC frequently even when there is a half spare memory on my computer. Isabelle/ML just used about 3 GB mem while my PC had 8GB spare mem and 19G spare swap (totally it has 16 GB mem and 20GB swap). The GC is frequent and starts to affect my working efficiency. Sometimes I have to reopen Isabelle to stop endless GC procedure. I wanna know, is this an issue or just some misconfiguration of mine?

view this post on Zulip Robert Soeldner (Aug 26 2022 at 13:01):

Hi Qiyuan,
I do see a similar behaviour.

view this post on Zulip Manuel Eberl (Aug 27 2022 at 14:25):

Infrastructure-related questions like these are better asked on the mailing list, because Makarius does not read Zulip. Maybe ask there and repeat how much memory you have. And also what OS and what kind of thing you are working on when this happens (i.e. is it a big development with lots of open theories?) Also any custom Isabelle options you may have set in ~/.isabelle/etc.


Last updated: Apr 19 2024 at 01:05 UTC