Re: [isabelle] Stray processes on Windows
On Sat, 23 Nov 2013, Gottfried Barrow wrote:
I'm not having problems now, but then, I'm not demanding much of the
PIDE because I've got done what I wanted. Surely, though, it was related
to export_code because the file was so small, and commenting in and out
"export_code" was about all I was doing.
A few more remarks, after looking once again over the external process
management of Isabelle/Scala and Isabelle/ML.
Process management according to POSIX only allows flat (non-nested)
process groups and asynchronous (unacknowledged) signals to kill another
process. To give the appearance of managed hierarchies of processes, the
Isabelle framework implements certain common-sense heuristics that usually
work, but implicitly depend on a reasonable degree of reactivity.
Under heavy load, though, a process that is signalled to terminate, but
remains unresponspive for too long, is killed the hard way. Thus it has
no chance to terminate its sub-processes properly.
This explains why an abrupt termination of the outermost PIDE application
can leave some external processes at the bottom of the hierarchy behind.
This archive was generated by a fusion of
Pipermail (Mailman edition) and