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.


	Makarius





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