Max Nowak (Mar 02 2021 at 22:44): Max Nowak (Mar 02 2021 at 22:44):Ever since upgrading to the new Isabelle2021, occasionally my the "zulu architecture" takes about 100% cpu usage, likely triggered by typing some proofs, not even necessarily try or anything. The only option is to close Isabelle, and 2/3 times it works. But occasionally the proof search processes (z3,...) never exit, and I need to restart my whole PC. Has anyone run into similar issues? I'm on Windows x64 on fairly recent hardware.
Max Nowak (Mar 03 2021 at 00:00):This seems to be a common pattern (usage drops to 0 since I quit isabelle)
Mathias Fleury (Mar 03 2021 at 05:53):Any specific reason to assume z3 is responsible?
Mathias Fleury (Mar 03 2021 at 05:56):Anyway, next time you start Isabelle, can you open the Monitor (bottom right, double click on ML) and look what happens on the ML side when it freezes? I saw this kind of things happen before on large theories and very slow GCing, but that might be something different.
Mathias Fleury (Mar 03 2021 at 06:06):What kind of formalization are you doing?
Mathias Fleury (Mar 03 2021 at 06:08):Max Nowak said:
This seems to be a common pattern (usage drops to 0 since I quit isabelle)
I am not familiar with the windows task manager. Is that one CPU or all CPUs? Does 100% mean every core is used?
Max Nowak (Mar 03 2021 at 23:17):That is all CPUs. No particular reason why z3, but it tends to happen when I use try or even just normal typing, and... hm, random realization: it tends to happen particularly often when I edit something at the beginning of a long proof, so maybe isabelle/hol tries spawning very heavy proof searches for all the now-broken subsequent proof steps, and hence lags a bunch?
Max Nowak (Mar 03 2021 at 23:18):I am not sure what to look for in the ML window.
Mathias Fleury (Mar 04 2021 at 06:05):In the ML window, look at the heap panel and if see anything suspicious (I don't know what to expect either). For example, you might see that GC is happening every 0.3 seconds, indicating that polyml needs more memory
Mathias Fleury (Mar 04 2021 at 06:08):When editing long proof and something breaks, I add a oops to make sure Isabelle is not running something (like metis or blast).
Max Nowak (Mar 04 2021 at 10:44):ML isn't the issue I think, it's got to be something else. Looking into the java monitoring console, I spotted a thread which seems to be running a solver all the time, even though there's nothing to do currently in my file, the stack trace is never in any waiting method, and instead always in kodkod.engine.Solver.solve() or deeper. And exactly one of my cores is currently fully loaded, so I assume it's just this thread too? Gut feeling tells me there's some issue killing the solvers once they're no longer needed and/or starting too many. Or maybe it's just an intended background task.
Mathias Fleury (Mar 04 2021 at 10:48):I know that some threads have moved from ML to Scala (aka java), like Kodkod. But I have no idea what happens in your case. You could try to deactivate auto_nitpick, but I don't know if this helps
Lukas Stevens (Mar 04 2021 at 10:49):I have a similar problem in Isabelle2020 when editing a file with two long proofs. After some time Isabelle greys out repeatedly but without Isabelle nor the system going out of memory. It is especially surprising since the file does not depend on other theories and the file itself is not too long (~700 lines).
Max Nowak (Mar 04 2021 at 10:53):Same theories, but isabelle2020 and everything is just fine for me.
Mathias Fleury (Mar 04 2021 at 11:54):If it is kodkod-Scala specifically, you could try Isabelle/jEdit > Plugins > Plugins options. Then Plugin Options > Isabelle > General > Miscellaneous Tools > untick kodkod scala
pandaman (Mar 08 2021 at 05:38):Hi! I stumbled upon this thread and tried monitoring my long-running theory. The theory takes several minutes at apply (auto simp add: Let_def), and the heap monitor shows the "zigzag" behavior at the time. Is this something that can be mitigated by adjusting the config, rewriting the proof, etc.? image.png
Mathias Fleury (Mar 08 2021 at 05:48):Rewrite the proof.
Max Nowak (Mar 08 2021 at 14:15):The heap monitor always shows a zigzag for me, no matter what I do. I assumed that is normal behaviour though?
Mathias Fleury (Mar 08 2021 at 18:24):the zigzag is normal. In big applications, memory pressure increases and you expect at some point a full GC where the allocated memory increases (the red curve)
Manuel Eberl (Mar 08 2021 at 18:28):I think the official recommendation is that if you have to open the memory monitor for any reason, you should buy more RAM. :big_smile:
I have 16 GB on my laptop and that's usually enough. My desktop has 32 GB and that's pretty much always enough. Less than 16 GB can be a bit problematic (although I, too, wonder why Isabell needs that much memory…)
pandaman (Mar 09 2021 at 04:41):Thank you for the answer. I already have 32GB of RAM and tried to tweak ISABELLE_TOOL_JAVA_OPTIONS and ML_OPTIONS, but it didn't change the behavior (maybe I should have closed the browser).
It seems that the expansion of the let expression is behaving exponentially, so I will try to work around this during the proof.
Fabian Huch (Mar 09 2021 at 08:46):To change the settings for the java process inIsabelle/jEdit, you have to set JEDIT_JAVA_OPTIONS (at least in a repository version).
Manuel Eberl (Mar 09 2021 at 09:30):Indeed, if 32 GB isn't enough, you really should change the proof.
Last updated: Apr 19 2024 at 04:17 UTC