diff -r 818cec5f82a4 -r a7258e1020b7 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Thu Oct 06 10:14:22 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Fri Oct 07 11:29:24 2005 +0200 @@ -16,8 +16,7 @@ (* Send request to Watcher for multiple spasses to be called for filenames in arg *) (* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *) -val callResProvers : - TextIO.outstream * (string*string*string*string) list -> unit +val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit (* Send message to watcher to kill resolution provers *) val callSlayer : TextIO.outstream -> unit @@ -39,8 +38,6 @@ val command_sep = #"\t" and setting_sep = #"%"; -open Recon_Transfer - val goals_being_watched = ref 0; val trace_path = Path.basic "watcher_trace"; @@ -48,18 +45,18 @@ fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s else (); -(* The result of calling createWatcher *) -datatype proc = PROC of {pid : Posix.Process.pid, - instr : TextIO.instream, - outstr : TextIO.outstream}; +(*Representation of a watcher process*) +type proc = {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*) - cmd: string, (* The file containing the goal for res prover to prove *) +(*Representation of a child (ATP) process*) +type cmdproc = { + prover: string, (* Name of the resolution prover used, e.g. "spass"*) + file: string, (* The file containing the goal for the ATP to prove *) proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc, - instr : TextIO.instream, (* Input stream to child process *) - outstr : TextIO.outstream}; (* Output stream from child process *) + instr : TextIO.instream, (*Output of the child process *) + outstr : TextIO.outstream}; (*Input to the child process *) fun fdReader (name : string, fd : Posix.IO.file_desc) = @@ -83,55 +80,25 @@ TextIO.StreamIO.mkInstream ( fdReader (name, fd), "")); -fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr)); - -fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr); - -fun cmdInStream (CMDPROC{instr,outstr,...}) = instr; - -fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,instr,outstr}) = - (prover,(cmd, (instr,outstr))); - -fun cmdchildHandle (CMDPROC{prover,cmd,proc_handle,instr,outstr}) = - proc_handle; - -fun cmdProver (CMDPROC{prover,cmd,proc_handle,instr,outstr}) = prover; - - -(* 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 *) - +(* 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) -(*****************************************************************************************) -(* Send request to Watcher for multiple provers to be called for filenames in arg *) -(* need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*) -(*****************************************************************************************) - +(* Send request to Watcher for multiple provers to be called*) fun callResProvers (toWatcherStr, []) = (TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr) -| callResProvers (toWatcherStr, + | callResProvers (toWatcherStr, (prover,proverCmd,settings,probfile) :: args) = - let val _ = trace (space_implode ", " - (["\ncallResProvers:", prover, proverCmd, probfile])) - in TextIO.output (toWatcherStr, - (*Uses a special character to separate items sent to watcher*) - space_implode (str command_sep) - [prover, proverCmd, settings, probfile, "\n"]); - goals_being_watched := (!goals_being_watched) + 1; - TextIO.flushOut toWatcherStr; - callResProvers (toWatcherStr,args) - end + (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile])); + (*Uses a special character to separate items sent to watcher*) + TextIO.output (toWatcherStr, + space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]); + goals_being_watched := (!goals_being_watched) + 1; + TextIO.flushOut toWatcherStr; + callResProvers (toWatcherStr,args)) - - (*Send message to watcher to kill currently running vampires. NOT USED and possibly buggy. Note that killWatcher kills the entire process group anyway.*) @@ -139,9 +106,7 @@ TextIO.flushOut toWatcherStr) -(**************************************************************) -(* Get commands from Isabelle *) -(**************************************************************) +(* Get commands from Isabelle*) fun getCmds (toParentStr, fromParentStr, cmdList) = let val thisLine = TextIO.inputLine fromParentStr in @@ -167,10 +132,7 @@ end -(**************************************************************) (* Get Io-descriptor for polling of an input stream *) -(**************************************************************) - fun getInIoDesc someInstr = let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr) val _ = TextIO.output (TextIO.stdOut, buf) @@ -189,19 +151,11 @@ (* Set up a Watcher Process *) (*************************************) -(* for tracing: encloses each string element in brackets. *) -val concat_with_and = space_implode " & " o map (enclose "(" ")"); - -fun prems_string_of th = concat_with_and (map string_of_cterm (cprems_of th)) - fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc); 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 => @@ -242,8 +196,7 @@ val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid} (*set process group id: allows killing all children*) val () = trace "\nsubgoals forked to startWatcher" - - fun pollChildInput fromStr = + fun pollChild fromStr = case getInIoDesc fromStr of SOME iod => (case OS.IO.pollDesc iod of @@ -255,57 +208,50 @@ end | NONE => false) | NONE => false - (* Check all ATP processes currently running for output *) fun checkChildren ([], toParentStr) = [] (* no children to check *) | checkChildren (childProc::otherChildren, toParentStr) = let val _ = trace ("\nIn check child, length of queue:"^ Int.toString (length (childProc::otherChildren))) - val (childInput,childOutput) = cmdstreamsOf childProc - val child_handle = cmdchildHandle childProc - val childCmd = #1(#2(cmdchildInfo childProc)) (*name of problem file*) - val _ = trace ("\nchildCmd = " ^ childCmd) - val sg_num = number_from_filename childCmd - val childIncoming = pollChildInput childInput - val parentID = Posix.ProcEnv.getppid() - val prover = cmdProver childProc + val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = + childProc + val _ = trace ("\nprobfile = " ^ file) + val sgno = number_from_filename file + val ppid = Posix.ProcEnv.getppid() in - if childIncoming + if pollChild childIn then (* check here for prover label on child*) - let val _ = trace ("\nInput available from child: " ^ childCmd ^ - "\nprover is " ^ prover) + let val _ = trace ("\nInput available from child: " ^ file) val childDone = (case prover of - "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID, childCmd, clause_arr) - | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID, childCmd, clause_arr) - | "spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID, childCmd, thm, sg_num,clause_arr) - | _ => (trace "\nBad prover!"; true) ) + "vampire" => AtpCommunication.checkVampProofFound + (childIn, toParentStr, ppid, file, clause_arr) + | "E" => AtpCommunication.checkEProofFound + (childIn, toParentStr, ppid, file, clause_arr) + | "spass" => AtpCommunication.checkSpassProofFound + (childIn, toParentStr, ppid, file, thm, sgno,clause_arr) + | _ => (trace ("\nBad prover! " ^ prover); true) ) in - if childDone - then (* child has found a proof and transferred it *) - (* Remove this child and go on to check others*) - (Unix.reap child_handle; - OS.FileSys.remove childCmd; - checkChildren(otherChildren, toParentStr)) + if childDone (*child has found a proof and transferred it*) + then (*Remove this child and go on to check others*) + (Unix.reap proc_handle; OS.FileSys.remove file; + checkChildren(otherChildren, toParentStr)) else (* Keep this child and go on to check others *) childProc :: checkChildren (otherChildren, toParentStr) end else (trace "\nNo child output"; childProc::(checkChildren (otherChildren, toParentStr))) end - (* call resolution processes *) - (* settings should be a list of strings ["-t 300", "-m 100000"] *) - (* takes list of (string, string, string list, string)list proclist *) + (* settings should be a list of strings ["-t300", "-m100000"] *) fun execCmds [] procList = procList | execCmds ((prover,proverCmd,settings,file)::cmds) procList = - let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ - file) + let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file) val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(proverCmd, settings@[file]) val (instr, outstr) = Unix.streamsOf childhandle - val newProcList = CMDPROC{prover = prover, - cmd = file, + val newProcList = {prover = prover, + file = file, proc_handle = childhandle, instr = instr, outstr = outstr} :: procList @@ -316,50 +262,53 @@ (******** Watcher Loop ********) val limit = ref 200; (*don't let it run forever*) - fun keepWatching (procList) = - let fun loop procList = - let val _ = trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^ - " length(procList) = " ^ Int.toString (length procList)); - val cmdsFromIsa = pollParentInput - (fromParentIOD, fromParentStr, toParentStr) - in - OS.Process.sleep (Time.fromMilliseconds 100); - limit := !limit - 1; - if !limit = 0 - then - (trace "\nTimeout: Killing proof processes"; - TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); - TextIO.flushOut toParentStr; - killChildren (map cmdchildHandle procList); - Posix.Process.exit 0w0) - else case cmdsFromIsa of - SOME [(_,"Kill children",_,_)] => - let val child_handles = map cmdchildHandle procList - in trace "\nReceived command to kill children"; - killChildren child_handles; loop [] - end - | SOME cmds => (* deal with commands from Isabelle process *) - if length procList < 40 - then (* Execute locally *) - let - val _ = trace ("\nCommands from parent: " ^ Int.toString(length cmds)) - val newProcList = execCmds cmds procList - val newProcList' = checkChildren (newProcList, toParentStr) - in - trace "\nCommands executed"; loop newProcList' - end - else (* Execute remotely [FIXME: NOT REALLY] *) - let - val newProcList = execCmds cmds procList - val newProcList' = checkChildren (newProcList, toParentStr) - in loop newProcList' end - | NONE => (* No new input from Isabelle *) - let val newProcList = checkChildren (procList, toParentStr) - in - trace "\nNothing from parent, still watching"; loop newProcList - end - end - in loop procList end + fun keepWatching procList = + let val _ = trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^ + " length(procList) = " ^ Int.toString (length procList)); + val cmdsFromIsa = pollParentInput + (fromParentIOD, fromParentStr, toParentStr) + in + OS.Process.sleep (Time.fromMilliseconds 100); + limit := !limit - 1; + if !limit < 0 + then + (trace "\nTimeout: Killing proof processes"; + TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); + TextIO.flushOut toParentStr; + killChildren (map #proc_handle procList); + Posix.Process.exit 0w0) + else + case cmdsFromIsa of + SOME [(_,"Kill children",_,_)] => + let val child_handles = map #proc_handle procList + in trace "\nReceived command to kill children"; + killChildren child_handles; keepWatching [] + end + | SOME cmds => (* deal with commands from Isabelle process *) + if length procList < 40 + then (* Execute locally *) + let + val _ = trace("\nCommands from parent: " ^ + Int.toString(length cmds)) + val newProcList = execCmds cmds procList + val newProcList' = checkChildren (newProcList, toParentStr) + in + trace "\nCommands executed"; keepWatching newProcList' + end + else (* Execute remotely [FIXME: NOT REALLY] *) + let + val newProcList = execCmds cmds procList + val newProcList' = checkChildren (newProcList, toParentStr) + in keepWatching newProcList' end + | NONE => (* No new input from Isabelle *) + let val newProcList = checkChildren (procList, toParentStr) + in trace "\nNothing from parent, still watching"; + keepWatching newProcList + end + end + handle exn => (*FIXME: exn handler is too general!*) + (trace ("\nkeepWatching: In exception handler: " ^ Toplevel.exn_message exn); + keepWatching procList); in (*** Sort out pipes ********) Posix.IO.close (#outfd p1); Posix.IO.close (#infd p2); @@ -381,7 +330,7 @@ (* 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]); - PROC{pid = pid, instr = instr, outstr = outstr} + {pid = pid, instr = instr, outstr = outstr} end; @@ -390,7 +339,18 @@ (* Start a watcher and set up signal handlers *) (**********************************************************) -fun killWatcher pid = Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill); +fun reapAll s = (*Signal handler to tidy away dead processes*) + (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of + SOME _ => reapAll s | NONE => ()) + handle OS.SysErr _ => () + +(*FIXME: does the main process need something like this? + IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*) + +fun killWatcher pid = + (goals_being_watched := 0; + Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill); + reapAll()); fun reapWatcher(pid, instr, outstr) = ignore (TextIO.closeIn instr; TextIO.closeOut outstr; @@ -401,25 +361,27 @@ string_of_cterm (List.nth(cprems_of th, i-1)) handle Subscript => "Subgoal number out of range!" +fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th)) + fun createWatcher (th, clause_arr) = - let val (childpid,(childin,childout)) = childInfo (setupWatcher(th,clause_arr)) + let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (th,clause_arr) fun decr_watched() = (goals_being_watched := !goals_being_watched - 1; if !goals_being_watched = 0 then (debug ("\nReaping a watcher, childpid = "^ - LargeWord.toString (Posix.Process.pidToWord childpid)); - killWatcher childpid; reapWatcher (childpid,childin, childout)) + Int.toString (ResLib.intOfPid childpid)); + killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) ) else ()) val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of th); fun proofHandler n = let val outcome = TextIO.inputLine childin val probfile = TextIO.inputLine childin - val sg_num = number_from_filename probfile - val text = string_of_subgoal th sg_num + val sgno = number_from_filename probfile + val text = string_of_subgoal th sgno val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ "\"\nprobfile = " ^ probfile ^ - "\ngoals_being_watched: "^ Int.toString (!goals_being_watched)) + "\nGoals being watched: "^ Int.toString (!goals_being_watched)) in if String.isPrefix "[" outcome (*indicates a proof reconstruction*) then (priority (Recon_Transfer.apply_res_thm outcome);