On Wed, 12 May 2010, Michael Norrish wrote:
Cygwin is not really relevant, but I suppose that, out of idle curiosity, it would nice to know if Posix.Process.exec worked there.
I have checked the (long) mail exchange with David from 2 years ago, when we sorted out many issues to make it work the way it is in Isabelle2008 or later, until today.
Attached is an earlier experiment involving straight-forward fork/exec with join/kill operations. Here is an example on Cygwin:
ML> elapsed_time (fn () => join (fork "true")) (); 0.719
That's almost a second penalty. The delay depends on various factors, including the size of the running ML process. The best I can get here is approx. 0.4 seconds.
On Linux on the same hardware class the result is like that:
ML> elapsed_time (fn () => join (fork "true")) (); 0.102
These 100ms are somehow intrinsic to the way the Poly/ML runtime system invokes external processes. David can explain that better. (I wonder if the builtin delay loop is still required these days.)
Makarius