Re: [isabelle] Stray processes on Windows
- To: Gottfried Barrow <gottfried.barrow at gmx.com>
- Subject: Re: [isabelle] Stray processes on Windows
- From: Makarius <makarius at sketis.net>
- Date: Sun, 1 Dec 2013 20:59:45 +0100 (CET)
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <alpine.LSU.firstname.lastname@example.org>
- References: <alpine.LSU.email@example.com> <528FFA44.firstname.lastname@example.org> <alpine.LSU.email@example.com> <5290CC37.firstname.lastname@example.org> <alpine.LSU.email@example.com>
- User-agent: Alpine 2.11 (LSU 23 2013-08-11)
On Sat, 23 Nov 2013, Makarius wrote:
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 should be resolved in Isabelle2013-2-RC3 -- I won't blame Stephan
Schulz again for his creative signal handlers in the C code of E Prover.
As long as you stay within Isabelle/jEdit, external processes should be
terminated eventually. When you close the Windows application while the
prover process is really busy with external loads, there is the old danger
of dangling tail ends of such processes.
What is missing here for future releases: a proper PIDE application
shutdown phase that notiates with the prover process via the PIDE
protocol, not crude POSIX signals.
This archive was generated by a fusion of
Pipermail (Mailman edition) and