Re: [isabelle] Stray processes on Windows

On Sat, 23 Nov 2013, Gottfried Barrow wrote:

From the time I was studying the processes of Sledgehammer, my notes show that metis is run by poly.exe, and metis is called by different ATPs.

Also, the extra poly.exe I mentioned was because I had an additional view open in the PIDE, which I forgot about. When I closed it, the poly.exe was terminated.

Note that the Prover IDE is connected to a single Isabelle/ML process (poly.exe) the whole time. Multiple editor views, buffers etc. don't matter. Things are different when you run multiple Isabelle.exe Windows applications at the same time, of course.

Metis is always run internally in the same prover process as anything else.

SML export_code runs a different, isolated poly.exe each time it is invoked.

Lots of poly.exe's get called. With Isabelle2012 (or Isabelle2011-1), something like eprover.exe would be left running sometimes, but I don't think I've seen that lately.

I still do see stray eprover processes, also on Unix platforms. This is probably a remaining problem of Stephan Schulz.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.