On 05/06/17 10:35, [email protected] 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/bash.ML http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/src/Pure/System/bash.scala http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/Admin/bash_process/bash_process.c 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 _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
