When I run
isabelle build on a non-trivial project, Isabelle tends to virtually take over my system, making other work difficult. It’s particularly bad when having a video call running concurrently. In this situation, the build typically takes much longer than usual and the video call effectively stops (basically no audio and video transmission anymore) and is finally dropped because of some timeout.
Initially, I thought that perhaps the scheduler assigns almost all CPU time to Isabelle’s threads, because Isabelle apparently wants to perform a lot of computation. However, this would be a bit stupid, and I find it hard to believe that Linux, which I’m using, can’t do a better scheduling job after 30 years of development. Recently, a colleague suggested that the problem I’m experiencing might have to do with RAM shortage instead.
In any case, are others here experiencing the same issue, and does someone know what the cause of this issue might be?
I would also guess RAM, Linux then has to start swapping to disk which is slow. You could try to use cgroups or containers (aka cgroups in disguise) to limit the RAM that isabelle has access to, e.g.:
cgcreate -g memory:isabelle echo 500M > /sys/fs/cgroup/memory/isabelle/memory.limit_in_bytes cgexec -g memory:isabelle isabelle build
(Adjust the 500M to a more suitable value ofc). Might need to install a package, on Ubuntu
Otherwise systemd makes this a bit easier:
systemd-run --scope -p MemoryMax=500M --user isabelle build
Thanks a lot. This seems to be helpful indeed.
Did I get this correctly that your solution boils down to letting Isabelle suffer from swapping more, while having other software, like the one for your video calls, suffer from swapping less or not at all?
Wolfgang Jeltsch has marked this topic as resolved.
Wolfgang Jeltsch has marked this topic as unresolved.
Theoretically yes, but in practice it should just run the garbage collection more often
Last updated: Dec 07 2023 at 08:19 UTC