[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 include below.

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 commands.

With Isabelle2013, rarely did processes get started that weren't terminated.

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 processes.

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 MHonArc.