equal
deleted
inserted
replaced
24 (* Start a watcher and set up signal handlers *) |
24 (* Start a watcher and set up signal handlers *) |
25 val createWatcher : |
25 val createWatcher : |
26 thm * string Array.array -> |
26 thm * string Array.array -> |
27 TextIO.instream * TextIO.outstream * Posix.Process.pid |
27 TextIO.instream * TextIO.outstream * Posix.Process.pid |
28 val killWatcher : Posix.Process.pid -> unit |
28 val killWatcher : Posix.Process.pid -> unit |
|
29 val killChild : ('a, 'b) Unix.proc -> OS.Process.status |
29 val setting_sep : char |
30 val setting_sep : char |
|
31 val reapAll : unit -> unit |
30 end |
32 end |
31 |
33 |
32 |
34 |
33 |
35 |
34 structure Watcher: WATCHER = |
36 structure Watcher: WATCHER = |
225 (childIn, toParentStr, ppid, file, names_arr) |
227 (childIn, toParentStr, ppid, file, names_arr) |
226 | "spass" => AtpCommunication.checkSpassProofFound |
228 | "spass" => AtpCommunication.checkSpassProofFound |
227 (childIn, toParentStr, ppid, file, th, sgno,names_arr) |
229 (childIn, toParentStr, ppid, file, th, sgno,names_arr) |
228 | _ => (trace ("\nBad prover! " ^ prover); true) ) |
230 | _ => (trace ("\nBad prover! " ^ prover); true) ) |
229 in |
231 in |
230 if childDone (*child has found a proof and transferred it*) |
232 if childDone (*ATP has reported back (with success OR failure)*) |
231 then (Unix.reap proc_handle; OS.FileSys.remove file; |
233 then (Unix.reap proc_handle; OS.FileSys.remove file; |
232 check children) |
234 check children) |
233 else child :: check children |
235 else child :: check children |
234 end |
236 end |
235 else (trace "\nNo child output"; child :: check children) |
237 else (trace "\nNo child output"; child :: check children) |
236 end |
238 end |
318 |
320 |
319 (**********************************************************) |
321 (**********************************************************) |
320 (* Start a watcher and set up signal handlers *) |
322 (* Start a watcher and set up signal handlers *) |
321 (**********************************************************) |
323 (**********************************************************) |
322 |
324 |
323 fun reapAll s = (*Signal handler to tidy away dead processes*) |
325 (*Signal handler to tidy away zombie processes*) |
|
326 fun reapAll() = |
324 (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of |
327 (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of |
325 SOME _ => reapAll s | NONE => ()) |
328 SOME _ => reapAll() | NONE => ()) |
326 handle OS.SysErr _ => () |
329 handle OS.SysErr _ => () |
327 |
330 |
328 (*FIXME: does the main process need something like this? |
331 (*FIXME: does the main process need something like this? |
329 IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*) |
332 IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*) |
330 |
333 |