I've investigated this and pushed a fix to master. I'll include it in
the fixes branch if it all seems fine.
David
On 05/04/2019 12:44, Norrish, Michael (Data61, Acton) wrote:
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
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml