[isabelle] Stray processes on Windows
On Fri, 22 Nov 2013, Gottfried Barrow wrote:
In general, I've seen that with Isabelle2013-1 and the RC versions, a
poly.exe process will many times get started and never get terminated,
and end up running at about 95% of the CPU.
Does that mean it is a left-over poly.exe process after you stop
Isabelle/jEdit, or are there additional instances of poly.exe while you
run the Prover IDE?
It has been Sledgehammer that I've mainly associated that with, but
today, I was using the command "export_code" in a simple theory, which I
I would say that Sledgehammer and export_code are quite different. I did
see occasional left-over process from Sledgehammer on Windows, notably E
prover, but that is not poly.exe.
The export_code command is special since it writes out given files
physically. As long as you continue typing, it will do it for several
prefixes of the file name. I can't tell if this can lock up the IDE.
You can try switching the new option "Continuous checking" off -- there is
a checkbox in the Theories panel and a keyboard shortcut C+e ENTER.
This is slightly awkward handiwork, and you must not forget to turn it on
again for checking things, but it might help with occasional stateful
With Isabelle2013, rarely did processes get started that weren't
In principle, I made several things in the process management more robust.
Some of that could cause new problems nonetheless.
Isabelle2013-1 also has an updated version of Cygwin, which could in
principle be less reliable than the one we've had before. This has
happened before, but so far there is no proof for that.
After I closed jEdit, a bunch of processes terminated, including a poly.exe,
but these 4 processes were still running:
This looks like the normal collection of processes for the prover backend.
Normally, stopping jEdit and its Isabelle/jEdit plugin should terminate
the processes as well. There is also a global JVM shutdown handler:
regular termination of the Java runtime should dispose any add-on
This does not work though, if the JVM is in bad state and needs to be
terminated the hard way, i.e. the light is switched of with the hammer.
This archive was generated by a fusion of
Pipermail (Mailman edition) and