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
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
SML export_code runs a different, isolated poly.exe each time it is
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