Email Gateway (Jan 14 2026 at 20:35): Email Gateway (Jan 14 2026 at 20:35):From: Peter Lammich <lammich@in.tum.de>
Dear List,
I recently encountered my fan not stopping to spin. I wanted to delete
the veriT threads, but found out that there was a poly thread sitting at
100% CPU, and not stopping. According to the theory panel, all theories
where completely processed, and according to the status bar, no GCs
where in progress.
I'd expect no 100% CPU thread in this situation ... restarting Isabelle
solved the problem.
What information can/shall I collect the next time that happens, in
order to identify the reason?
--
Peter
OS: Ubuntu on x86_64
Email Gateway (Jan 15 2026 at 10:04):From: Makarius <makarius@sketis.net>
On 14/01/2026 21:34, Peter Lammich wrote:
What information can/shall I collect the next time that happens, in order to
identify the reason?
Maybe some information from "top" about memory: VIRT, RES.
Also a confirmation that the "poly" process is really the prover backend, not
the ML runtime monitor process.
You can see the difference via "ps aux | grep poly". The monitor has a
command-line like this:
poly -q --use src/Pure/ML/ml_statistics.ML --eval ML_Statistics.monitor
5617 0.5
Makarius
Email Gateway (Jan 18 2026 at 11:53):From: Makarius <makarius@sketis.net>
On 18/01/2026 07:35, Vincent Jackson wrote:
Here is my current Isabelle version:
isabelle version -it
4b875a4c83b0
Isabelle2025
That is already outdated. We are talking about Isabelle2025-1 here.
Maybe some information from "top" about memory: VIRT, RES.
Also a confirmation that the "poly" process is really the prover backend,
not the ML runtime monitor process.
Here is the requested information:admin 145198 261 22.9 7786296 3698832 ? Sl 16:04 21:19 poly -q --minheap 1000 --gcthreads 4 --exportstats --eval (PolyML.SaveState.loadHierarchy ["<...>/Isabelle2025/heaps/polyml-for-isabelle-2025_x86_64-linux/Pure", "<...>/Isabelle2025/heaps/polyml-for-isabelle-2025_x86_64-linux/HOL"]; PolyML.print_depth 0) --eval Options.load_default () --eval Resources.init_session_env () --eval Isabelle_Process.init ()
admin 145229 0.0 0.1 2586568 25312 ? Sl 16:05 0:00 poly -q --use src/Pure/ML/ml_statistics.ML --eval ML_Statistics.monitor 145198 0.5
For claritiy, here are is the ps header line (on Linux):
USER PID %CPU %MEM VSZ RSS TTY STAT START TIME COMMAND
It means that the poly process above is running at 261% --- which is a notable
difference from the initial observation on this thread. 100% often means that
a there is a single thread that "hangs".
The scale for the process size is unclear to me. Maybe we see approx. 3.6 GiB
above, which is not so much. (Assuming this is decent hardware with 16..32 GiB
total.)
I have also noticed that whenever this does happen, the ML status indicator in
jEdit reads "ML cleanup", but I have no idea if that's diagnostically relevant.
That means poly is running garbage collection. It can take quite long, but
should finish eventually. If it doesn't, it needs further investigation ---
using a current version of Isabelle --- with an authentic Poly/ML component
that has been provided by the Isabelle distribution.
Makarius
Email Gateway (Jan 19 2026 at 22:09):From: Vincent Jackson <vjjac@student.unimelb.edu.au>
Hello, I am also experiencing this issue.
Here is my current Isabelle version:
isabelle version -it
4b875a4c83b0
Isabelle2025
Maybe some information from "top" about memory: VIRT, RES.
Also a confirmation that the "poly" process is really the prover
backend, not the ML runtime monitor process.
Here is the requested information:
admin 145198 261 22.9 7786296 3698832 ? Sl 16:04 21:19 poly -q --minheap 1000 --gcthreads 4 --exportstats --eval (PolyML.SaveState.loadHierarchy ["<...>/Isabelle2025/heaps/polyml-for-isabelle-2025_x86_64-linux/Pure", "<...>/Isabelle2025/heaps/polyml-for-isabelle-2025_x86_64-linux/HOL"]; PolyML.print_depth 0) --eval Options.load_default () --eval Resources.init_session_env () --eval Isabelle_Process.init ()
admin 145229 0.0 0.1 2586568 25312 ? Sl 16:05 0:00 poly -q --use src/Pure/ML/ml_statistics.ML --eval ML_Statistics.monitor 145198 0.5
(N.b. I have trimmed some excessively long paths generated by nixos.)
I have also noticed that whenever this does happen, the ML status
indicator in jEdit reads "ML cleanup", but I have no idea if that's
diagnostically relevant.
Vincent
Last updated: Jan 31 2026 at 12:53 UTC