HOL4's Holmake tool uses a fork/exec idiom to run scripts in parallel (and to monitor their output file descriptors). Under 5.8 this code is causing signal 11 failures (segmentation faults), as reported by a few users, and apparent also on runs on Travis such as https://travis-ci.org/HOL-Theorem-Prover/HOL/jobs/515996149 (It is apparent from the related Travis pages that the same sources are running to completion perfectly with 5.7.1.)
The code for doing the fork/exec stuff is visible at https://github.com/HOL-Theorem-Prover/HOL/blob/8990db3c7743feb190d98f4bce666d3163022557/tools/Holmake/poly/ProcessMultiplexor.sml#L152-L190 This code also works under mlton (although eventually does cause "out of filedescriptor" syscall failures because mlton won't garbage collect my fds after they stop getting used), so I do feel as if the code should work. The failures all happen when Holmake is first run in this mode. When forced to run single-threaded with its -j1 option, which makes it use OS.Process.system underneath, Holmake can work. Michael _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
