As per
https://travis-ci.org/HOL-Theorem-Prover/HOL/jobs/516807586
This looks good for Holmake; thanks!
Michael
On 7 Apr 2019, at 17:30, David Matthews <David.Matthews at prolingua.co.uk<mailto:David.Matthews at prolingua.co.uk>> wrote:
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/8990db3c7743feb190d98f4bce666... 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 at inf.ed.ac.uk<mailto:polyml at inf.ed.ac.uk> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml