# HG changeset patch # User paulson # Date 1127320519 -7200 # Node ID e93f7510e1e1da0abafd478e5d55564abf0d3c9f # Parent 20c0b69dd1927d4d005f798af9dda7f156a000e2 trying to limit the looping diff -r 20c0b69dd192 -r e93f7510e1e1 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Wed Sep 21 18:06:04 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Wed Sep 21 18:35:19 2005 +0200 @@ -16,36 +16,24 @@ signature WATCHER = sig -(*****************************************************************************************) (* Send request to Watcher for multiple spasses to be called for filenames in arg *) -(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *) -(*****************************************************************************************) +(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *) val callResProvers : TextIO.outstream * (string*string*string*string*string) list -> unit -(************************************************************************) (* Send message to watcher to kill currently running resolution provers *) -(************************************************************************) - val callSlayer : TextIO.outstream -> unit -(**********************************************************) (* Start a watcher and set up signal handlers *) -(**********************************************************) - val createWatcher : thm * (ResClause.clause * thm) Array.array -> TextIO.instream * TextIO.outstream * Posix.Process.pid -(**********************************************************) (* Kill watcher process *) -(**********************************************************) - val killWatcher : Posix.Process.pid -> unit val killWatcher' : int -> unit - end @@ -57,42 +45,32 @@ val goals_being_watched = ref 0; -(*****************************************) (* The result of calling createWatcher *) -(*****************************************) - datatype proc = PROC of { pid : Posix.Process.pid, instr : TextIO.instream, outstr : TextIO.outstream }; -(*****************************************) (* The result of calling executeToList *) -(*****************************************) - datatype cmdproc = CMDPROC of { - prover: string, (* Name of the resolution prover used, e.g. Vampire, SPASS *) - cmd: string, (* The file containing the goal for res prover to prove *) - goalstring: string, (* string representation of subgoal*) + prover: string, (* Name of the resolution prover used, e.g. Vampire*) + cmd: string, (* The file containing the goal for res prover to prove *) + goalstring: string, (* string representation of subgoal*) proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc, instr : TextIO.instream, (* Input stream to child process *) - outstr : TextIO.outstream (* Output stream from child process *) - }; + outstr : TextIO.outstream}; (* Output stream from child process *) type signal = Posix.Signal.signal datatype exit_status = datatype Posix.Process.exit_status val fromStatus = Posix.Process.fromStatus - fun reap(pid, instr, outstr) = let val u = TextIO.closeIn instr; val u = TextIO.closeOut outstr; val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) - in - status - end + in status end fun fdReader (name : string, fd : Posix.IO.file_desc) = Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd }; @@ -134,19 +112,14 @@ goalstring; -(********************************************************************************) (* gets individual args from instream and concatenates them into a list *) -(********************************************************************************) - fun getArgs (fromParentStr, toParentStr, ys) = let val thisLine = TextIO.input fromParentStr in ys@[thisLine] end -(********************************************************************************) (* Send request to Watcher for a vampire to be called for filename in arg *) -(********************************************************************************) - + fun callResProver (toWatcherStr, arg) = (TextIO.output (toWatcherStr, arg^"\n"); TextIO.flushOut toWatcherStr) @@ -223,21 +196,17 @@ let val thisLine = TextIO.inputLine fromParentStr val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine in - if thisLine = "End of calls\n" then cmdList + if thisLine = "End of calls\n" orelse thisLine = "" then cmdList else if thisLine = "Kill children\n" - then - ( TextIO.output (toParentStr,thisLine ); - TextIO.flushOut toParentStr; - (("","","Kill children",[],"")::cmdList) - ) + then (TextIO.output (toParentStr,thisLine ); + TextIO.flushOut toParentStr; + (("","","Kill children",[],"")::cmdList) ) else let val thisCmd = getCmd thisLine (*********************************************************) (* thisCmd = (prover,proverCmd, settings, file)*) (* i.e. put back into tuple format *) (*********************************************************) in - (*TextIO.output (toParentStr, thisCmd); - TextIO.flushOut toParentStr;*) getCmds (toParentStr, fromParentStr, thisCmd::cmdList) end end @@ -274,6 +243,24 @@ fun killChildren procs = List.app (ignore o killChild) procs; + (*************************************************************) + (* take an instream and poll its underlying reader for input *) + (*************************************************************) + + fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = + case OS.IO.pollDesc fromParentIOD + of SOME pd => + let val pd' = OS.IO.pollIn pd + val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) + in + if null pdl + then NONE + else if OS.IO.isIn (hd pdl) + then SOME (getCmds (toParentStr, fromParentStr, [])) + else NONE + end + | NONE => NONE; + fun setupWatcher (thm,clause_arr) = let (** pipes for communication between parent and watcher **) @@ -302,30 +289,7 @@ val fromParentStr = openInFD ("_exec_in_parent", fromParent) val toParentStr = openOutFD ("_exec_out_parent", toParent) val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm); - - (*************************************************************) - (* take an instream and poll its underlying reader for input *) - (*************************************************************) - - fun pollParentInput () = - let val pd = OS.IO.pollDesc fromParentIOD - in - if isSome pd then - let val pd' = OS.IO.pollIn (valOf pd) - val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) - val _ = File.append (File.tmp_path (Path.basic "parent_poll")) - ("In parent_poll\n") - in - if null pdl - then - NONE - else if (OS.IO.isIn (hd pdl)) - then SOME (getCmds (toParentStr, fromParentStr, [])) - else NONE - end - else NONE - end - + fun pollChildInput fromStr = let val _ = File.append (File.tmp_path (Path.basic "child_poll")) ("In child_poll\n") @@ -345,7 +309,7 @@ NONE) else if OS.IO.isIn (hd pdl) then - let val inval = (TextIO.inputLine fromStr) + let val inval = TextIO.inputLine fromStr val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n") in SOME inval end else @@ -355,21 +319,23 @@ else NONE end else NONE - end - + end - (****************************************************************************) - (* Check all vampire processes currently running for output *) - (****************************************************************************) + val cc_iterations_left = ref 50; + (*FIXME: why does this loop if not explicitly bounded?*) + + (* Check all ATP processes currently running for output *) (*********************************) fun checkChildren ([], toParentStr) = [] (*** no children to check ********) (*********************************) | checkChildren ((childProc::otherChildren), toParentStr) = let val _ = File.append (File.tmp_path (Path.basic "child_check")) ("In check child, length of queue:"^ - string_of_int (length (childProc::otherChildren))) - val (childInput,childOutput) = cmdstreamsOf childProc - val child_handle= cmdchildHandle childProc + Int.toString (length (childProc::otherChildren)) ^ + "\niterations left = " ^ Int.toString (!cc_iterations_left)) + val _ = Posix.Process.sleep (Time.fromMilliseconds 50) (*slow the looping*) + val (childInput,childOutput) = cmdstreamsOf childProc + val child_handle = cmdchildHandle childProc (* childCmd is the .dfg file that the problem is in *) val childCmd = fst(snd (cmdchildInfo childProc)) val _ = File.append (File.tmp_path (Path.basic "child_check")) @@ -395,11 +361,16 @@ ("\nsubgoals forked to checkChildren: " ^ space_implode "\n" [prems_string,prover,goalstring]) in - if isSome childIncoming + cc_iterations_left := !cc_iterations_left - 1; + if !cc_iterations_left = 0 then [] (*Abandon looping!*) + else if isSome childIncoming then (* check here for prover label on child*) let val _ = File.append (File.tmp_path (Path.basic "child_check")) - "\nInput available from childIncoming" + ("\nInput available from childIncoming" ^ + "\nchecking if proof found." ^ + "\nchildCmd is " ^ childCmd ^ + "\ngoalstring is: " ^ goalstring ^ "\n\n") val childDone = (case prover of "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr) | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr) @@ -478,17 +449,23 @@ (**********************************************) (* Watcher Loop *) (**********************************************) - val iterations_left = ref 1000; (*200 seconds, 5 iterations per sec*) + val iterations_left = ref 100; (*don't let it run forever*) - fun keepWatching (toParentStr, fromParentStr,procList) = + fun keepWatching (procList) = let fun loop procList = let val _ = Posix.Process.sleep (Time.fromMilliseconds 200) - val cmdsFromIsa = pollParentInput () + val _ = File.append (File.tmp_path (Path.basic "keep_watch")) + ("\nCalling pollParentInput: " ^ + Int.toString (!iterations_left)); + val cmdsFromIsa = pollParentInput + (fromParentIOD, fromParentStr, toParentStr) in iterations_left := !iterations_left - 1; - if !iterations_left = 0 + if !iterations_left <= 0 then (*Sadly, this code fails to terminate the watcher!*) - (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); + (File.append (File.tmp_path (Path.basic "keep_watch")) + "\nTimeout: Killing proof processes"; + TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); TextIO.flushOut toParentStr; killChildren (map cmdchildHandle procList)) else if isSome cmdsFromIsa @@ -505,20 +482,21 @@ then (* Execute locally *) let val newProcList = execCmds (valOf cmdsFromIsa) procList - val parentID = Posix.ProcEnv.getppid() - val _ = File.append (File.tmp_path (Path.basic "prekeep_watch")) - "Just execed a child\n" + val _ = Posix.ProcEnv.getppid() + val _ = File.append (File.tmp_path (Path.basic "keep_watch")) + "\nJust execed a child" val newProcList' = checkChildren (newProcList, toParentStr) in File.append (File.tmp_path (Path.basic "keep_watch")) - "Off to keep watching...\n"; + ("\nOff to keep watching: " ^ + Int.toString (!iterations_left)); loop newProcList' end else (* Execute remotely *) (* (actually not remote for now )*) let val newProcList = execCmds (valOf cmdsFromIsa) procList - val parentID = Posix.ProcEnv.getppid() + val _ = Posix.ProcEnv.getppid() val newProcList' =checkChildren (newProcList, toParentStr) in loop newProcList' @@ -526,7 +504,9 @@ else (* No new input from Isabelle *) let val newProcList = checkChildren (procList, toParentStr) in - (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...2\n "); + File.append (File.tmp_path (Path.basic "keep_watch")) + ("\nNo new input, still watching: " ^ + Int.toString (!iterations_left)); loop newProcList end end @@ -550,7 +530,7 @@ (***************************) (* start the watcher loop *) (***************************) - keepWatching (toParentStr, fromParentStr, procList); + keepWatching (procList); (****************************************************************************) (* fake return value - actually want the watcher to loop until killed *) (****************************************************************************) @@ -574,24 +554,21 @@ val instr = openInFD ("_exec_in", #infd p2) val outstr = openOutFD ("_exec_out", #outfd p1) - in - (*******************************) - (* close the child-side fds *) - (*******************************) - Posix.IO.close (#outfd p2); - Posix.IO.close (#infd p1); - (* set the fds close on exec *) - Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); - Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); - - (*******************************) - (* return value *) - (*******************************) - PROC{pid = pid, - instr = instr, - outstr = outstr - } - end; + in + (*******************************) + (* close the child-side fds *) + (*******************************) + Posix.IO.close (#outfd p2); + Posix.IO.close (#infd p1); + (* set the fds close on exec *) + Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); + Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); + + (*******************************) + (* return value *) + (*******************************) + PROC{pid = pid, instr = instr, outstr = outstr} + end; @@ -624,7 +601,7 @@ val goalstring = TextIO.inputLine childin val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ "\"\ngoalstring = " ^ goalstring ^ - "\ngoals_being_watched: "^ string_of_int (!goals_being_watched)) + "\ngoals_being_watched: "^ Int.toString (!goals_being_watched)) in if String.isPrefix "[" outcome (*indicates a proof reconstruction*) then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));