# HG changeset patch # User paulson # Date 1128690508 -7200 # Node ID 0ecfb66ea072e571e38afc09f2de19c0e70aff0e # Parent a7258e1020b70880ff6d715709142ca16167f50f code restructuring diff -r a7258e1020b7 -r 0ecfb66ea072 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Fri Oct 07 11:29:24 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Fri Oct 07 15:08:28 2005 +0200 @@ -132,13 +132,13 @@ end -(* Get Io-descriptor for polling of an input stream *) +(*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) val ioDesc = case rd - of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod + of TextPrimIO.RD{ioDesc = SOME iod, ...} => SOME iod | _ => NONE in (* since getting the reader will have terminated the stream, we need * to build a new stream. *) @@ -146,6 +146,19 @@ ioDesc end +fun pollChild fromStr = + case getInIoDesc fromStr of + SOME iod => + (case OS.IO.pollDesc iod of + SOME pd => + let val pd' = OS.IO.pollIn pd in + case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of + [] => false + | pd''::_ => OS.IO.isIn pd'' + end + | NONE => false) + | NONE => false + (*************************************) (* Set up a Watcher Process *) @@ -153,18 +166,25 @@ fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc); -fun killChildren procs = List.app (ignore o killChild) procs; +val killChildren = List.app (ignore o killChild o #proc_handle) : cmdproc list -> unit; + +fun killWatcher (toParentStr, procList) = + (trace "\nWatcher timeout: Killing proof processes"; + TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); + TextIO.flushOut toParentStr; + killChildren procList; + Posix.Process.exit 0w0); - (* take an instream and poll its underlying reader for input *) - fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = - case OS.IO.pollDesc fromParentIOD of - SOME pd => - (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of - [] => NONE - | pd''::_ => if OS.IO.isIn pd'' - then SOME (getCmds (toParentStr, fromParentStr, [])) - else NONE) - | NONE => NONE; +(* take an instream and poll its underlying reader for input *) +fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = + case OS.IO.pollDesc fromParentIOD of + SOME pd => + (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of + [] => NONE + | pd''::_ => if OS.IO.isIn pd'' + then SOME (getCmds (toParentStr, fromParentStr, [])) + else NONE) + | NONE => NONE; (*get the number of the subgoal from the filename: the last digit string*) fun number_from_filename s = @@ -173,151 +193,112 @@ raise ERROR) | numbers => valOf (Int.fromString (List.last numbers)); -fun setupWatcher (thm,clause_arr) = +(* call ATP. 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) + val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = + Unix.execute(proverCmd, settings@[file]) + val (instr, outstr) = Unix.streamsOf childhandle + val newProcList = {prover=prover, file=file, proc_handle=childhandle, + instr=instr, outstr=outstr} :: procList + val _ = trace ("\nFinished at " ^ + Date.toString(Date.fromTimeLocal(Time.now()))) + in execCmds cmds newProcList end + +fun checkChildren (th, clause_arr, toParentStr, children) = + let fun check [] = [] (* no children to check *) + | check (child::children) = + let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = + child + val _ = trace ("\nprobfile = " ^ file) + val sgno = number_from_filename file + val ppid = Posix.ProcEnv.getppid() + in + if pollChild childIn + then (* check here for prover label on child*) + let val _ = trace ("\nInput available from child: " ^ file) + val childDone = (case prover of + "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, th, sgno,clause_arr) + | _ => (trace ("\nBad prover! " ^ prover); true) ) + in + if childDone (*child has found a proof and transferred it*) + then (Unix.reap proc_handle; OS.FileSys.remove file; + check children) + else child :: check children + end + else (trace "\nNo child output"; child :: check children) + end + in + trace ("\nIn checkChildren, length of queue: " ^ Int.toString(length children)); + check children + end; + + +fun setupWatcher (th,clause_arr) = let val p1 = Posix.IO.pipe() (*pipes for communication between parent and watcher*) val p2 = Posix.IO.pipe() - fun closep () = - (Posix.IO.close (#outfd p1); Posix.IO.close (#infd p1); - Posix.IO.close (#outfd p2); Posix.IO.close (#infd p2)) (****** fork a watcher process and get it set up and going ******) fun startWatcher procList = - (case Posix.Process.fork() - of SOME pid => pid (* parent - i.e. main Isabelle process *) - | NONE => let (* child - i.e. watcher *) - val oldchildin = #infd p1 - val fromParent = Posix.FileSys.wordToFD 0w0 - val oldchildout = #outfd p2 - val toParent = Posix.FileSys.wordToFD 0w1 - val fromParentIOD = Posix.FileSys.fdToIOD fromParent - val fromParentStr = openInFD ("_exec_in_parent", fromParent) - val toParentStr = openOutFD ("_exec_out_parent", toParent) - val pid = Posix.ProcEnv.getpid() - 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 pollChild fromStr = - case getInIoDesc fromStr of - SOME iod => - (case OS.IO.pollDesc iod of - SOME pd => - let val pd' = OS.IO.pollIn pd in - case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of - [] => false - | pd''::_ => OS.IO.isIn pd'' - 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 {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 pollChild childIn - then (* check here for prover label on child*) - let val _ = trace ("\nInput available from child: " ^ file) - val childDone = (case prover of - "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 (*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 ["-t300", "-m100000"] *) - fun execCmds [] procList = procList - | execCmds ((prover,proverCmd,settings,file)::cmds) procList = - 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 = {prover = prover, - file = file, - proc_handle = childhandle, - instr = instr, - outstr = outstr} :: procList - val _ = trace ("\nFinished at " ^ - Date.toString(Date.fromTimeLocal(Time.now()))) - in execCmds cmds newProcList end - - (******** Watcher Loop ********) - val limit = ref 200; (*don't let it run forever*) - - 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); - Posix.IO.dup2{old = oldchildin, new = fromParent}; - Posix.IO.close oldchildin; - Posix.IO.dup2{old = oldchildout, new = toParent}; - Posix.IO.close oldchildout; - keepWatching (procList) - end); (* end case *) + case Posix.Process.fork() of + SOME pid => pid (* parent - i.e. main Isabelle process *) + | NONE => + let (* child - i.e. watcher *) + val oldchildin = #infd p1 + val fromParent = Posix.FileSys.wordToFD 0w0 + val oldchildout = #outfd p2 + val toParent = Posix.FileSys.wordToFD 0w1 + val fromParentIOD = Posix.FileSys.fdToIOD fromParent + val fromParentStr = openInFD ("_exec_in_parent", fromParent) + val toParentStr = openOutFD ("_exec_out_parent", toParent) + val pid = Posix.ProcEnv.getpid() + val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid} + (*set process group id: allows killing all children*) + val () = trace "\nsubgoals forked to startWatcher" + val limit = ref 200; (*don't let watcher run forever*) + (*Watcher Loop : Check running ATP processes for output*) + fun keepWatching procList = + (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^ + " length(procList) = " ^ Int.toString(length procList)); + OS.Process.sleep (Time.fromMilliseconds 100); limit := !limit - 1; + if !limit < 0 then killWatcher (toParentStr, procList) + else + case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of + SOME [(_,"Kill children",_,_)] => + (trace "\nReceived Kill command"; + killChildren procList; keepWatching []) + | 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' = checkChildren(th, clause_arr, toParentStr, + execCmds cmds procList) + in trace "\nCommands executed"; keepWatching newProcList' end + else (* Execute remotely [FIXME: NOT REALLY] *) + let val newProcList' = checkChildren (th, clause_arr, toParentStr, + execCmds cmds procList) + in keepWatching newProcList' end + | NONE => (* No new input from Isabelle *) + (trace "\nNothing from parent..."; + keepWatching(checkChildren(th, clause_arr, toParentStr, procList)))) + handle exn => (*FIXME: exn handler is too general!*) + (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn); + keepWatching procList); + in + (*** Sort out pipes ********) + Posix.IO.close (#outfd p1); Posix.IO.close (#infd p2); + Posix.IO.dup2{old = oldchildin, new = fromParent}; + Posix.IO.close oldchildin; + Posix.IO.dup2{old = oldchildout, new = toParent}; + Posix.IO.close oldchildout; + keepWatching (procList) + end; val _ = TextIO.flushOut TextIO.stdOut val pid = startWatcher []