On 05/06/17 10:35, Michael.Norrish at data61.csiro.au wrote:
Both this (with Posix.Process open):
case fork() of NONE => (exece(proc,proc::args,env')
and this:
case fork() of exece(executable,nm_args,env)seem to be causing us grief, particularly on a recent Linux, PolyML 5.7 and under conditions of some memory load.
Is there a better idiom we might use?
For Isabelle, I have made many variations and refinements in the past 10 years -- without fork/exec due to portability problems. The present state in this quest for perfection is here (both for ML and Scala):
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/src/Pure/System... http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/src/Pure/System... http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/Admin/bash_proc...
The main idea is to use plain OS.Process.system (Posix) or Windows.simpleExecute with a Thread.fork around it. Thus a synchronous process execution is management asynchronously by a separate thread.
In the implementation, the basic idea of Process.system + Thread.fork is further complicated due to requirements for:
* uniform use of bash on all platforms (including Debian/Ubuntu and Windows) * proper handling of signals (interrupts) * management of the external process as a group * timing information for the external process
Makarius