112 |
112 |
113 fun openInFD (name, fd) = |
113 fun openInFD (name, fd) = |
114 TextIO.mkInstream ( |
114 TextIO.mkInstream ( |
115 TextIO.StreamIO.mkInstream ( |
115 TextIO.StreamIO.mkInstream ( |
116 fdReader (name, fd), "")); |
116 fdReader (name, fd), "")); |
117 |
|
118 fun killChild child_handle = Unix.reap child_handle |
|
119 |
117 |
120 fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr)); |
118 fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr)); |
121 |
119 |
122 fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr); |
120 fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr); |
123 |
121 |
270 fun getProofCmd (a,c,d,e,f) = d |
268 fun getProofCmd (a,c,d,e,f) = d |
271 |
269 |
272 fun prems_string_of th = |
270 fun prems_string_of th = |
273 Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th)) |
271 Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th)) |
274 |
272 |
|
273 fun killChildren procs = List.app (ignore o Unix.reap) procs; |
|
274 |
275 fun setupWatcher (thm,clause_arr) = |
275 fun setupWatcher (thm,clause_arr) = |
276 let |
276 let |
277 (** pipes for communication between parent and watcher **) |
277 (** pipes for communication between parent and watcher **) |
278 val p1 = Posix.IO.pipe () |
278 val p1 = Posix.IO.pipe () |
279 val p2 = Posix.IO.pipe () |
279 val p2 = Posix.IO.pipe () |
298 val toParent = Posix.FileSys.wordToFD 0w1 |
298 val toParent = Posix.FileSys.wordToFD 0w1 |
299 val fromParentIOD = Posix.FileSys.fdToIOD fromParent |
299 val fromParentIOD = Posix.FileSys.fdToIOD fromParent |
300 val fromParentStr = openInFD ("_exec_in_parent", fromParent) |
300 val fromParentStr = openInFD ("_exec_in_parent", fromParent) |
301 val toParentStr = openOutFD ("_exec_out_parent", toParent) |
301 val toParentStr = openOutFD ("_exec_out_parent", toParent) |
302 val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm); |
302 val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm); |
303 fun killChildren [] = () |
|
304 | killChildren (child_handle::children) = |
|
305 (killChild child_handle; killChildren children) |
|
306 |
303 |
307 (*************************************************************) |
304 (*************************************************************) |
308 (* take an instream and poll its underlying reader for input *) |
305 (* take an instream and poll its underlying reader for input *) |
309 (*************************************************************) |
306 (*************************************************************) |
310 |
307 |
483 |
480 |
484 fun keepWatching (toParentStr, fromParentStr,procList) = |
481 fun keepWatching (toParentStr, fromParentStr,procList) = |
485 let fun loop procList = |
482 let fun loop procList = |
486 let val _ = Posix.Process.sleep (Time.fromMilliseconds 200) |
483 let val _ = Posix.Process.sleep (Time.fromMilliseconds 200) |
487 val cmdsFromIsa = pollParentInput () |
484 val cmdsFromIsa = pollParentInput () |
488 fun killchildHandler () = |
|
489 (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); |
|
490 TextIO.flushOut toParentStr; |
|
491 killChildren (map cmdchildHandle procList); |
|
492 ()) |
|
493 in |
485 in |
494 (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*) |
|
495 iterations_left := !iterations_left - 1; |
486 iterations_left := !iterations_left - 1; |
496 if !iterations_left = 0 then killchildHandler () |
487 if !iterations_left = 0 |
|
488 then (*Sadly, this code fails to terminate the watcher!*) |
|
489 (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); |
|
490 TextIO.flushOut toParentStr; |
|
491 killChildren (map cmdchildHandle procList)) |
497 else if isSome cmdsFromIsa |
492 else if isSome cmdsFromIsa |
498 then (* deal with input from Isabelle *) |
493 then (* deal with input from Isabelle *) |
499 if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" |
494 if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" |
500 then |
495 then |
501 let val child_handles = map cmdchildHandle procList |
496 let val child_handles = map cmdchildHandle procList |
502 in |
497 in |
503 killChildren child_handles; |
498 killChildren child_handles; |
504 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) |
|
505 loop [] |
499 loop [] |
506 end |
500 end |
507 else |
501 else |
508 if length procList < 5 (********************) |
502 if length procList < 5 (********************) |
509 then (* Execute locally *) |
503 then (* Execute locally *) |
612 Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ()) |
606 Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ()) |
613 |
607 |
614 fun createWatcher (thm, clause_arr) = |
608 fun createWatcher (thm, clause_arr) = |
615 let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr)) |
609 let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr)) |
616 fun decr_watched() = |
610 fun decr_watched() = |
617 (goals_being_watched := (!goals_being_watched) - 1; |
611 (goals_being_watched := !goals_being_watched - 1; |
618 if !goals_being_watched = 0 |
612 if !goals_being_watched = 0 |
619 then |
613 then |
620 (File.append (File.tmp_path (Path.basic "reap_found")) |
614 (File.append (File.tmp_path (Path.basic "reap_found")) |
621 ("Reaping a watcher, childpid = "^ |
615 ("Reaping a watcher, childpid = "^ |
622 LargeWord.toString (Posix.Process.pidToWord childpid)^"\n"); |
616 LargeWord.toString (Posix.Process.pidToWord childpid)^"\n"); |
627 let val outcome = TextIO.inputLine childin |
621 let val outcome = TextIO.inputLine childin |
628 val goalstring = TextIO.inputLine childin |
622 val goalstring = TextIO.inputLine childin |
629 val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ |
623 val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ |
630 "\"\ngoalstring = " ^ goalstring ^ |
624 "\"\ngoalstring = " ^ goalstring ^ |
631 "\ngoals_being_watched: "^ string_of_int (!goals_being_watched)) |
625 "\ngoals_being_watched: "^ string_of_int (!goals_being_watched)) |
632 in (* if a proof has been found and sent back as a reconstruction proof *) |
626 in |
633 if String.isPrefix "[" outcome |
627 if String.isPrefix "[" outcome (*indicates a proof reconstruction*) |
634 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
628 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
635 Recon_Transfer.apply_res_thm outcome goalstring; |
629 Recon_Transfer.apply_res_thm outcome goalstring; |
636 Pretty.writeln(Pretty.str (oct_char "361")); |
630 Pretty.writeln(Pretty.str (oct_char "361")); |
637 decr_watched()) |
631 decr_watched()) |
638 (* if there's no proof, but a message from the signalling process*) |
|
639 else if String.isPrefix "Invalid" outcome |
632 else if String.isPrefix "Invalid" outcome |
640 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
633 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
641 Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) |
634 Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) |
642 ^ "is not provable")); |
635 ^ "is not provable")); |
643 Pretty.writeln(Pretty.str (oct_char "361")); |
636 Pretty.writeln(Pretty.str (oct_char "361")); |