--- 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);