--- a/src/HOL/Tools/ATP/watcher.ML Thu Oct 06 10:13:34 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Thu Oct 06 10:14:22 2005 +0200
@@ -17,8 +17,7 @@
(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
val callResProvers :
- TextIO.outstream * (string*string*string*string*string) list
- -> unit
+ TextIO.outstream * (string*string*string*string) list -> unit
(* Send message to watcher to kill resolution provers *)
val callSlayer : TextIO.outstream -> unit
@@ -50,31 +49,18 @@
else ();
(* The result of calling createWatcher *)
-datatype proc = PROC of {
- pid : Posix.Process.pid,
- instr : TextIO.instream,
- outstr : TextIO.outstream
- };
+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*)
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 *)
-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
fun fdReader (name : string, fd : Posix.IO.file_desc) =
Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
@@ -103,17 +89,13 @@
fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
-fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) =
+fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,instr,outstr}) =
(prover,(cmd, (instr,outstr)));
-fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr}) =
+fun cmdchildHandle (CMDPROC{prover,cmd,proc_handle,instr,outstr}) =
proc_handle;
-fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr}) =
- prover;
-
-fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr}) =
- goalstring;
+fun cmdProver (CMDPROC{prover,cmd,proc_handle,instr,outstr}) = prover;
(* gets individual args from instream and concatenates them into a list *)
@@ -136,17 +118,13 @@
fun callResProvers (toWatcherStr, []) =
(TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr)
| callResProvers (toWatcherStr,
- (prover,goalstring, proverCmd,settings,
- probfile) :: args) =
- let val _ = trace (space_implode "\n"
- (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
- probfile]))
+ (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,
- String.toString goalstring ^ "\n"]);
- (*goalstring is a single string literal, with all specials escaped.*)
+ [prover, proverCmd, settings, probfile, "\n"]);
goals_being_watched := (!goals_being_watched) + 1;
TextIO.flushOut toWatcherStr;
callResProvers (toWatcherStr,args)
@@ -172,17 +150,16 @@
else if thisLine = "Kill children\n"
then (TextIO.output (toParentStr,thisLine);
TextIO.flushOut toParentStr;
- [("","","Kill children",[],"")])
+ [("","Kill children",[],"")])
else
- let val [prover,proverCmd,settingstr,probfile,goalstring] =
+ let val [prover,proverCmd,settingstr,probfile,_] =
String.tokens (fn c => c = command_sep) thisLine
val settings = String.tokens (fn c => c = setting_sep) settingstr
in
- trace ("\nprover: " ^ prover ^ " prover path: " ^ proverCmd^
- " problem file: " ^ probfile ^
- "\ngoalstring: "^goalstring);
+ trace ("\nprover: " ^ prover ^ " prover path: " ^ proverCmd ^
+ "\n problem file: " ^ probfile);
getCmds (toParentStr, fromParentStr,
- (prover, goalstring, proverCmd, settings, probfile)::cmdList)
+ (prover, proverCmd, settings, probfile)::cmdList)
end
handle Bind =>
(trace "getCmds: command parsing failed!";
@@ -215,8 +192,7 @@
(* 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 (Sign.string_of_term (sign_of_thm th)) (prems_of th))
+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);
@@ -239,13 +215,14 @@
(*get the number of the subgoal from the filename: the last digit string*)
fun number_from_filename s =
case String.tokens (not o Char.isDigit) s of
- [] => (trace "\nWatcher could not read subgoal nunber!!"; raise ERROR)
+ [] => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
+ raise ERROR)
| numbers => valOf (Int.fromString (List.last numbers));
fun setupWatcher (thm,clause_arr) =
let
- val p1 = Posix.IO.pipe () (** pipes for communication between parent and watcher **)
- val p2 = Posix.IO.pipe ()
+ 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))
@@ -264,7 +241,7 @@
val pid = Posix.ProcEnv.getpid()
val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
(*set process group id: allows killing all children*)
- val () = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
+ val () = trace "\nsubgoals forked to startWatcher"
fun pollChildInput fromStr =
case getInIoDesc fromStr of
@@ -292,18 +269,16 @@
val childIncoming = pollChildInput childInput
val parentID = Posix.ProcEnv.getppid()
val prover = cmdProver childProc
- val prems_string = prems_string_of thm
- val goalstring = cmdGoal childProc
in
- trace("\nsubgoals forked to checkChildren: " ^ goalstring);
if childIncoming
then (* check here for prover label on child*)
let val _ = trace ("\nInput available from child: " ^ childCmd ^
- "\ngoalstring is " ^ goalstring)
+ "\nprover is " ^ prover)
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)
- |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr) )
+ "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) )
in
if childDone
then (* child has found a proof and transferred it *)
@@ -323,117 +298,89 @@
(* settings should be a list of strings ["-t 300", "-m 100000"] *)
(* takes list of (string, string, string list, string)list proclist *)
fun execCmds [] procList = procList
- | execCmds ((prover, goalstring,proverCmd,settings,file)::cmds) procList =
- let val _ = trace (space_implode "\n"
- (["\nAbout to execute command for goal:",
- goalstring, proverCmd] @ settings @
- [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
+ | 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 = CMDPROC{prover = prover,
cmd = file,
- goalstring = goalstring,
proc_handle = childhandle,
instr = instr,
outstr = outstr} :: procList
-
- val _ = trace ("\nFinished at " ^
+ val _ = trace ("\nFinished at " ^
Date.toString(Date.fromTimeLocal(Time.now())))
in execCmds cmds newProcList end
(******** Watcher Loop ********)
- val limit = ref 500; (*don't let it run forever*)
+ val limit = ref 200; (*don't let it run forever*)
fun keepWatching (procList) =
let fun loop procList =
- let val _ = trace ("\nCalling pollParentInput: " ^ Int.toString (!limit));
+ 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);
- exit 0)
- else case cmdsFromIsa of
- SOME [(_,_,"Kill children",_,_)] =>
- let val child_handles = map cmdchildHandle procList
- in killChildren child_handles; loop [] end
- | SOME cmds => (* deal with commands from Isabelle process *)
- if length procList < 40
- then (* Execute locally *)
- let
- val newProcList = execCmds cmds procList
- val newProcList' = checkChildren (newProcList, toParentStr)
- in
- trace "\nJust execed a child"; 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 "\nNo new input, still watching"; loop newProcList
- end
+ 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
-
-
+ in loop procList end
in
- (*** Sort out pipes ********)
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p2);
+ (*** 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;
-
- (* start the watcher loop *)
- keepWatching (procList);
- (* fake return value - actually want the watcher to loop until killed *)
- Posix.Process.wordToPid 0w0
- end);
- (* end case *)
-
+ keepWatching (procList)
+ end); (* end case *)
val _ = TextIO.flushOut TextIO.stdOut
-
- (*******************************)
- (*** set watcher going ********)
- (*******************************)
-
- val procList = []
- val pid = startWatcher procList
- (**************************************************)
- (* communication streams to watcher *)
- (**************************************************)
-
+ val pid = startWatcher []
+ (* communication streams to watcher*)
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);
+ (* 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;
@@ -445,12 +392,17 @@
fun killWatcher pid = Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
-fun reapWatcher(pid, instr, outstr) =
+fun reapWatcher(pid, instr, outstr) = ignore
(TextIO.closeIn instr; TextIO.closeOut outstr;
- Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
+ Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
+ handle OS.SysErr _ => ()
-fun createWatcher (thm, clause_arr) =
- let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
+fun string_of_subgoal th i =
+ string_of_cterm (List.nth(cprems_of th, i-1))
+ handle Subscript => "Subgoal number out of range!"
+
+fun createWatcher (th, clause_arr) =
+ let val (childpid,(childin,childout)) = childInfo (setupWatcher(th,clause_arr))
fun decr_watched() =
(goals_being_watched := !goals_being_watched - 1;
if !goals_being_watched = 0
@@ -459,30 +411,32 @@
LargeWord.toString (Posix.Process.pidToWord childpid));
killWatcher childpid; reapWatcher (childpid,childin, childout))
else ())
- val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
+ val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of th);
fun proofHandler n =
let val outcome = TextIO.inputLine childin
- val goalstring = valOf (String.fromString (TextIO.inputLine childin))
+ val probfile = TextIO.inputLine childin
+ val sg_num = number_from_filename probfile
+ val text = string_of_subgoal th sg_num
val _ = debug ("In signal handler. outcome = \"" ^ outcome ^
- "\"\ngoalstring = " ^ goalstring ^
+ "\"\nprobfile = " ^ probfile ^
"\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 goalstring);
+ then (priority (Recon_Transfer.apply_res_thm outcome);
decr_watched())
else if String.isPrefix "Invalid" outcome
- then (priority ("Subgoal is not provable:\n" ^ goalstring);
+ then (priority ("Subgoal is not provable:\n" ^ text);
decr_watched())
else if String.isPrefix "Failure" outcome
- then (priority ("Proof attempt failed:\n" ^ goalstring);
+ then (priority ("Proof attempt failed:\n" ^ text);
decr_watched())
(* print out a list of rules used from clasimpset*)
else if String.isPrefix "Success" outcome
- then (priority (outcome ^ goalstring);
+ then (priority (outcome ^ text);
decr_watched())
(* if proof translation failed *)
else if String.isPrefix "Translation failed" outcome
- then (priority (outcome ^ goalstring);
+ then (priority (outcome ^ text);
decr_watched())
else (priority "System error in proof handler";
decr_watched())