more tidying. Fixed process management bugs and race condition
authorpaulson
Fri Oct 07 11:29:24 2005 +0200 (2005-10-07)
changeset 17773a7258e1020b7
parent 17772 818cec5f82a4
child 17774 0ecfb66ea072
more tidying. Fixed process management bugs and race condition
src/HOL/Tools/ATP/AtpCommunication.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML	Thu Oct 06 10:14:22 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Fri Oct 07 11:29:24 2005 +0200
     1.3 @@ -19,6 +19,8 @@
     1.4      val checkSpassProofFound:  
     1.5            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
     1.6            string * thm * int * (ResClause.clause * thm) Array.array -> bool
     1.7 +    val signal_parent:  
     1.8 +          TextIO.outstream * Posix.Process.pid * string * string -> unit
     1.9    end;
    1.10  
    1.11  structure AtpCommunication : ATP_COMMUNICATION =
    1.12 @@ -94,7 +96,9 @@
    1.13    TextIO.output (toParent, probfile ^ "\n");
    1.14    TextIO.flushOut toParent;
    1.15    trace ("\nSignalled parent: " ^ msg ^ probfile);
    1.16 -  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
    1.17 +  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.18 +  (*Give the parent time to respond before possibly sending another signal*)
    1.19 +  OS.Process.sleep (Time.fromMilliseconds 600));
    1.20  
    1.21  (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
    1.22  fun checkVampProofFound (fromChild, toParent, ppid, probfile, clause_arr) =
    1.23 @@ -120,7 +124,7 @@
    1.24   in   
    1.25       trace thisLine;
    1.26       if thisLine = "" 
    1.27 -     then (trace "No proof output seen\n"; false)
    1.28 +     then (trace "\nNo proof output seen"; false)
    1.29       else if String.isPrefix start_E thisLine
    1.30       then      
    1.31         startTransfer (end_E, fromChild, toParent, ppid, probfile, clause_arr)
    1.32 @@ -199,7 +203,7 @@
    1.33   let val thisLine = TextIO.inputLine fromChild  
    1.34   in    
    1.35       trace thisLine;
    1.36 -     if thisLine = "" then (trace "No proof output seen\n"; false)
    1.37 +     if thisLine = "" then (trace "\nNo proof output seen"; false)
    1.38       else if thisLine = "SPASS beiseite: Proof found.\n"
    1.39       then      
    1.40          startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
     2.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Oct 06 10:14:22 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Oct 07 11:29:24 2005 +0200
     2.3 @@ -16,8 +16,7 @@
     2.4  (*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
     2.5  (* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
     2.6  
     2.7 -val callResProvers :
     2.8 -    TextIO.outstream * (string*string*string*string) list -> unit
     2.9 +val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit
    2.10  
    2.11  (* Send message to watcher to kill resolution provers *)
    2.12  val callSlayer : TextIO.outstream -> unit
    2.13 @@ -39,8 +38,6 @@
    2.14  val command_sep = #"\t"
    2.15  and setting_sep = #"%";
    2.16  
    2.17 -open Recon_Transfer
    2.18 -
    2.19  val goals_being_watched = ref 0;
    2.20  
    2.21  val trace_path = Path.basic "watcher_trace";
    2.22 @@ -48,18 +45,18 @@
    2.23  fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
    2.24                else ();
    2.25  
    2.26 -(*  The result of calling createWatcher  *)
    2.27 -datatype proc = PROC of {pid : Posix.Process.pid,
    2.28 -			 instr : TextIO.instream,
    2.29 -			 outstr : TextIO.outstream};
    2.30 +(*Representation of a watcher process*)
    2.31 +type proc = {pid : Posix.Process.pid,
    2.32 +             instr : TextIO.instream,
    2.33 +             outstr : TextIO.outstream};
    2.34  
    2.35 -(*  The result of calling executeToList  *)
    2.36 -datatype cmdproc = CMDPROC of {
    2.37 -        prover: string,       (* Name of the resolution prover used, e.g. Vampire*)
    2.38 -        cmd:  string,         (* The file containing the goal for res prover to prove *)     
    2.39 +(*Representation of a child (ATP) process*)
    2.40 +type cmdproc = {
    2.41 +        prover: string,       (* Name of the resolution prover used, e.g. "spass"*)
    2.42 +        file:  string,        (* The file containing the goal for the ATP to prove *)     
    2.43          proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    2.44 -        instr : TextIO.instream,   (*  Input stream to child process *)
    2.45 -        outstr : TextIO.outstream};  (*  Output stream from child process *)
    2.46 +        instr : TextIO.instream,     (*Output of the child process *)
    2.47 +        outstr : TextIO.outstream};  (*Input to the child process *)
    2.48  
    2.49  
    2.50  fun fdReader (name : string, fd : Posix.IO.file_desc) =
    2.51 @@ -83,55 +80,25 @@
    2.52  	    TextIO.StreamIO.mkInstream (
    2.53  	      fdReader (name, fd), ""));
    2.54  
    2.55 -fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
    2.56 -
    2.57 -fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
    2.58 -
    2.59 -fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
    2.60 -
    2.61 -fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,instr,outstr}) = 
    2.62 -  (prover,(cmd, (instr,outstr)));
    2.63 -
    2.64 -fun cmdchildHandle (CMDPROC{prover,cmd,proc_handle,instr,outstr})  = 
    2.65 -  proc_handle;
    2.66 -
    2.67 -fun cmdProver (CMDPROC{prover,cmd,proc_handle,instr,outstr}) = prover;
    2.68 -
    2.69 -
    2.70 -(*    gets individual args from instream and concatenates them into a list      *)
    2.71 -fun getArgs (fromParentStr, toParentStr, ys) =  
    2.72 -  let val thisLine = TextIO.input fromParentStr
    2.73 -  in ys@[thisLine] end
    2.74 -
    2.75                              
    2.76 -(*  Send request to Watcher for a vampire to be called for filename in arg      *)
    2.77 -                   
    2.78 +(*  Send request to Watcher for a vampire to be called for filename in arg*)
    2.79  fun callResProver (toWatcherStr,  arg) = 
    2.80        (TextIO.output (toWatcherStr, arg^"\n"); 
    2.81         TextIO.flushOut toWatcherStr)
    2.82  
    2.83 -(*****************************************************************************************)
    2.84 -(*  Send request to Watcher for multiple provers to be called for filenames in arg       *)
    2.85 -(*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
    2.86 -(*****************************************************************************************)
    2.87 -
    2.88 +(*  Send request to Watcher for multiple provers to be called*)
    2.89  fun callResProvers (toWatcherStr,  []) = 
    2.90        (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
    2.91 -|   callResProvers (toWatcherStr,
    2.92 +  | callResProvers (toWatcherStr,
    2.93                      (prover,proverCmd,settings,probfile)  ::  args) =
    2.94 -      let val _ = trace (space_implode ", " 
    2.95 -		         (["\ncallResProvers:", prover, proverCmd, probfile]))
    2.96 -      in TextIO.output (toWatcherStr,
    2.97 -                        (*Uses a special character to separate items sent to watcher*)
    2.98 -      	                space_implode (str command_sep)
    2.99 -                          [prover, proverCmd, settings, probfile, "\n"]);
   2.100 -         goals_being_watched := (!goals_being_watched) + 1;
   2.101 -	 TextIO.flushOut toWatcherStr;
   2.102 -	 callResProvers (toWatcherStr,args)
   2.103 -      end   
   2.104 +      (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile]));
   2.105 +       (*Uses a special character to separate items sent to watcher*)
   2.106 +       TextIO.output (toWatcherStr,
   2.107 +          space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
   2.108 +       goals_being_watched := (!goals_being_watched) + 1;
   2.109 +       TextIO.flushOut toWatcherStr;
   2.110 +       callResProvers (toWatcherStr,args))
   2.111                                                  
   2.112 -                                    
   2.113 - 
   2.114  
   2.115  (*Send message to watcher to kill currently running vampires. NOT USED and possibly
   2.116    buggy. Note that killWatcher kills the entire process group anyway.*)
   2.117 @@ -139,9 +106,7 @@
   2.118                              TextIO.flushOut toWatcherStr)
   2.119  
   2.120                      
   2.121 -(**************************************************************)
   2.122 -(* Get commands from Isabelle                                 *)
   2.123 -(**************************************************************)
   2.124 +(* Get commands from Isabelle*)
   2.125  fun getCmds (toParentStr, fromParentStr, cmdList) = 
   2.126    let val thisLine = TextIO.inputLine fromParentStr 
   2.127    in
   2.128 @@ -167,10 +132,7 @@
   2.129    end
   2.130  	    
   2.131                                                                    
   2.132 -(**************************************************************)
   2.133  (*  Get Io-descriptor for polling of an input stream          *)
   2.134 -(**************************************************************)
   2.135 -
   2.136  fun getInIoDesc someInstr = 
   2.137      let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   2.138          val _ = TextIO.output (TextIO.stdOut, buf)
   2.139 @@ -189,19 +151,11 @@
   2.140  (*  Set up a Watcher Process         *)
   2.141  (*************************************)
   2.142  
   2.143 -(* for tracing: encloses each string element in brackets. *)
   2.144 -val concat_with_and = space_implode " & " o map (enclose "(" ")");
   2.145 -
   2.146 -fun prems_string_of th = concat_with_and (map string_of_cterm (cprems_of th))
   2.147 -
   2.148  fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
   2.149  
   2.150  fun killChildren procs = List.app (ignore o killChild) procs;
   2.151  
   2.152 - (*************************************************************)
   2.153   (* take an instream and poll its underlying reader for input *)
   2.154 - (*************************************************************)
   2.155 - 
   2.156   fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = 
   2.157     case OS.IO.pollDesc fromParentIOD of
   2.158        SOME pd =>
   2.159 @@ -242,8 +196,7 @@
   2.160  	  val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
   2.161                     (*set process group id: allows killing all children*)
   2.162  	  val () = trace "\nsubgoals forked to startWatcher"
   2.163 -	 
   2.164 -	  fun pollChildInput fromStr = 
   2.165 +	  fun pollChild fromStr = 
   2.166  	     case getInIoDesc fromStr of
   2.167  	       SOME iod => 
   2.168  		 (case OS.IO.pollDesc iod of
   2.169 @@ -255,57 +208,50 @@
   2.170  			end
   2.171  		   | NONE => false)
   2.172  	     | NONE => false
   2.173 -
   2.174  	  (* Check all ATP processes currently running for output                 *)
   2.175  	  fun checkChildren ([], toParentStr) = []  (* no children to check *)
   2.176  	  |   checkChildren (childProc::otherChildren, toParentStr) = 
   2.177  	       let val _ = trace ("\nIn check child, length of queue:"^
   2.178  			          Int.toString (length (childProc::otherChildren)))
   2.179 -		   val (childInput,childOutput) = cmdstreamsOf childProc
   2.180 -		   val child_handle = cmdchildHandle childProc
   2.181 -		   val childCmd = #1(#2(cmdchildInfo childProc)) (*name of problem file*)
   2.182 -		   val _ = trace ("\nchildCmd = " ^ childCmd)
   2.183 -		   val sg_num = number_from_filename childCmd
   2.184 -		   val childIncoming = pollChildInput childInput
   2.185 -		   val parentID = Posix.ProcEnv.getppid()
   2.186 -		   val prover = cmdProver childProc
   2.187 +		   val {prover, file, proc_handle, instr=childIn, ...} : cmdproc =
   2.188 +		       childProc
   2.189 +		   val _ = trace ("\nprobfile = " ^ file)
   2.190 +		   val sgno = number_from_filename file
   2.191 +		   val ppid = Posix.ProcEnv.getppid()
   2.192  	       in 
   2.193 -		 if childIncoming
   2.194 +		 if pollChild childIn
   2.195  		 then (* check here for prover label on child*)
   2.196 -		   let val _ = trace ("\nInput available from child: " ^ childCmd ^ 
   2.197 -				      "\nprover is " ^ prover)
   2.198 +		   let val _ = trace ("\nInput available from child: " ^ file)
   2.199  		       val childDone = (case prover of
   2.200 -			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID, childCmd, clause_arr)  
   2.201 -		         | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID, childCmd, clause_arr)             
   2.202 -			 | "spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID, childCmd, thm, sg_num,clause_arr)  
   2.203 -			 | _ => (trace "\nBad prover!"; true) )
   2.204 +			   "vampire" => AtpCommunication.checkVampProofFound
   2.205 +			        (childIn, toParentStr, ppid, file, clause_arr)  
   2.206 +		         | "E" => AtpCommunication.checkEProofFound
   2.207 +		                (childIn, toParentStr, ppid, file, clause_arr)             
   2.208 +			 | "spass" => AtpCommunication.checkSpassProofFound
   2.209 +			        (childIn, toParentStr, ppid, file, thm, sgno,clause_arr)  
   2.210 +			 | _ => (trace ("\nBad prover! " ^ prover); true) )
   2.211  		    in
   2.212 -		     if childDone
   2.213 -		     then (* child has found a proof and transferred it *)
   2.214 -			(* Remove this child and go on to check others*)
   2.215 -			(Unix.reap child_handle;
   2.216 -			 OS.FileSys.remove childCmd;
   2.217 -			 checkChildren(otherChildren, toParentStr))
   2.218 +		     if childDone (*child has found a proof and transferred it*)
   2.219 +		     then (*Remove this child and go on to check others*)
   2.220 +		          (Unix.reap proc_handle; OS.FileSys.remove file;
   2.221 +			   checkChildren(otherChildren, toParentStr))
   2.222  		     else (* Keep this child and go on to check others  *)
   2.223  		       childProc :: checkChildren (otherChildren, toParentStr)
   2.224  		  end
   2.225  		else (trace "\nNo child output";
   2.226  		      childProc::(checkChildren (otherChildren, toParentStr)))
   2.227  	       end
   2.228 -
   2.229  	
   2.230  	(* call resolution processes                                        *)
   2.231 -	(* settings should be a list of strings  ["-t 300", "-m 100000"]    *)
   2.232 -	(* takes list of (string, string, string list, string)list proclist *)
   2.233 +	(* settings should be a list of strings  ["-t300", "-m100000"]    *)
   2.234  	fun execCmds [] procList = procList
   2.235  	|   execCmds ((prover,proverCmd,settings,file)::cmds) procList  =
   2.236 -	      let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ 
   2.237 -	                         file)
   2.238 +	      let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
   2.239  	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   2.240  		       Unix.execute(proverCmd, settings@[file])
   2.241  		  val (instr, outstr) = Unix.streamsOf childhandle
   2.242 -		  val newProcList = CMDPROC{prover = prover,
   2.243 -					    cmd = file,
   2.244 +		  val newProcList = {prover = prover,
   2.245 +					    file = file,
   2.246  					    proc_handle = childhandle,
   2.247  					    instr = instr,
   2.248  					    outstr = outstr} :: procList
   2.249 @@ -316,50 +262,53 @@
   2.250           (******** Watcher Loop ********)
   2.251           val limit = ref 200;  (*don't let it run forever*)
   2.252  
   2.253 -	 fun keepWatching (procList) = 
   2.254 -	   let fun loop procList =  
   2.255 -	      let val _ = trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^ 
   2.256 -	                         "  length(procList) = " ^ Int.toString (length procList));
   2.257 -		  val cmdsFromIsa = pollParentInput 
   2.258 -				     (fromParentIOD, fromParentStr, toParentStr)
   2.259 -	      in 
   2.260 -		OS.Process.sleep (Time.fromMilliseconds 100);
   2.261 -		limit := !limit - 1;
   2.262 -		if !limit = 0 
   2.263 -		then 
   2.264 -		 (trace "\nTimeout: Killing proof processes";
   2.265 -		  TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   2.266 -		  TextIO.flushOut toParentStr;
   2.267 -		  killChildren (map cmdchildHandle procList);
   2.268 -		  Posix.Process.exit 0w0)
   2.269 -		else case cmdsFromIsa of
   2.270 -		    SOME [(_,"Kill children",_,_)] => 
   2.271 -		      let val child_handles = map cmdchildHandle procList 
   2.272 -		      in  trace "\nReceived command to kill children";
   2.273 -			  killChildren child_handles; loop [] 
   2.274 -		      end
   2.275 -		  | SOME cmds => (*  deal with commands from Isabelle process *)
   2.276 -		      if length procList < 40
   2.277 -		      then                        (* Execute locally  *)
   2.278 -			let 
   2.279 -			  val _ = trace ("\nCommands from parent: " ^ Int.toString(length cmds))
   2.280 -			  val newProcList = execCmds cmds procList
   2.281 -			  val newProcList' = checkChildren (newProcList, toParentStr) 
   2.282 -			in
   2.283 -			  trace "\nCommands executed"; loop newProcList'
   2.284 -			end
   2.285 -		      else  (* Execute remotely [FIXME: NOT REALLY]  *)
   2.286 -			let 
   2.287 -			  val newProcList = execCmds cmds procList
   2.288 -			  val newProcList' = checkChildren (newProcList, toParentStr) 
   2.289 -			in loop newProcList' end
   2.290 -		  | NONE => (* No new input from Isabelle *)
   2.291 -		      let val newProcList = checkChildren (procList, toParentStr)
   2.292 -		      in
   2.293 -			trace "\nNothing from parent, still watching"; loop newProcList
   2.294 -		      end
   2.295 -	       end
   2.296 -	   in  loop procList   end
   2.297 +	 fun keepWatching procList = 
   2.298 +	   let val _ = trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^ 
   2.299 +			      "  length(procList) = " ^ Int.toString (length procList));
   2.300 +	       val cmdsFromIsa = pollParentInput 
   2.301 +				  (fromParentIOD, fromParentStr, toParentStr)
   2.302 +	   in 
   2.303 +	     OS.Process.sleep (Time.fromMilliseconds 100);
   2.304 +	     limit := !limit - 1;
   2.305 +	     if !limit < 0 
   2.306 +	     then 
   2.307 +	      (trace "\nTimeout: Killing proof processes";
   2.308 +	       TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   2.309 +	       TextIO.flushOut toParentStr;
   2.310 +	       killChildren (map #proc_handle procList);
   2.311 +	       Posix.Process.exit 0w0)
   2.312 +	     else 
   2.313 +	       case cmdsFromIsa of
   2.314 +		 SOME [(_,"Kill children",_,_)] => 
   2.315 +		   let val child_handles = map #proc_handle procList 
   2.316 +		   in  trace "\nReceived command to kill children";
   2.317 +		       killChildren child_handles; keepWatching [] 
   2.318 +		   end
   2.319 +	       | SOME cmds => (*  deal with commands from Isabelle process *)
   2.320 +		   if length procList < 40
   2.321 +		   then                        (* Execute locally  *)
   2.322 +		     let 
   2.323 +		       val _ = trace("\nCommands from parent: " ^ 
   2.324 +		                     Int.toString(length cmds))
   2.325 +		       val newProcList = execCmds cmds procList
   2.326 +		       val newProcList' = checkChildren (newProcList, toParentStr) 
   2.327 +		     in
   2.328 +		       trace "\nCommands executed"; keepWatching newProcList'
   2.329 +		     end
   2.330 +		   else  (* Execute remotely [FIXME: NOT REALLY]  *)
   2.331 +		     let 
   2.332 +		       val newProcList = execCmds cmds procList
   2.333 +		       val newProcList' = checkChildren (newProcList, toParentStr) 
   2.334 +		     in keepWatching newProcList' end
   2.335 +	       | NONE => (* No new input from Isabelle *)
   2.336 +		   let val newProcList = checkChildren (procList, toParentStr)
   2.337 +		   in trace "\nNothing from parent, still watching"; 
   2.338 +		      keepWatching newProcList
   2.339 +		   end
   2.340 +	   end
   2.341 +	   handle exn => (*FIXME: exn handler is too general!*)
   2.342 +	     (trace ("\nkeepWatching: In exception handler: " ^ Toplevel.exn_message exn);
   2.343 +	      keepWatching procList);
   2.344  	 in
   2.345  	   (*** Sort out pipes ********)
   2.346  	   Posix.IO.close (#outfd p1);  Posix.IO.close (#infd p2);
   2.347 @@ -381,7 +330,7 @@
   2.348      (* set the fds close on exec *)
   2.349      Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   2.350      Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   2.351 -    PROC{pid = pid, instr = instr, outstr = outstr}
   2.352 +    {pid = pid, instr = instr, outstr = outstr}
   2.353    end;
   2.354  
   2.355  
   2.356 @@ -390,7 +339,18 @@
   2.357  (* Start a watcher and set up signal handlers             *)
   2.358  (**********************************************************)
   2.359  
   2.360 -fun killWatcher pid = Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
   2.361 +fun reapAll s = (*Signal handler to tidy away dead processes*)
   2.362 +     (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
   2.363 +	  SOME _ => reapAll s | NONE => ()) 
   2.364 +     handle OS.SysErr _ => ()
   2.365 +
   2.366 +(*FIXME: does the main process need something like this?
   2.367 +    IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*)
   2.368 +
   2.369 +fun killWatcher pid = 
   2.370 +  (goals_being_watched := 0;
   2.371 +   Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
   2.372 +   reapAll());
   2.373  
   2.374  fun reapWatcher(pid, instr, outstr) = ignore
   2.375    (TextIO.closeIn instr; TextIO.closeOut outstr;
   2.376 @@ -401,25 +361,27 @@
   2.377      string_of_cterm (List.nth(cprems_of th, i-1))
   2.378      handle Subscript => "Subgoal number out of range!"
   2.379  
   2.380 +fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
   2.381 +
   2.382  fun createWatcher (th, clause_arr) =
   2.383 - let val (childpid,(childin,childout)) = childInfo (setupWatcher(th,clause_arr))
   2.384 + let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (th,clause_arr)
   2.385       fun decr_watched() =
   2.386  	  (goals_being_watched := !goals_being_watched - 1;
   2.387  	   if !goals_being_watched = 0
   2.388  	   then 
   2.389  	     (debug ("\nReaping a watcher, childpid = "^
   2.390 -		     LargeWord.toString (Posix.Process.pidToWord childpid));
   2.391 -	      killWatcher childpid; reapWatcher (childpid,childin, childout))
   2.392 +		     Int.toString (ResLib.intOfPid childpid));
   2.393 +	      killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
   2.394  	    else ())
   2.395       val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of th);
   2.396       fun proofHandler n = 
   2.397         let val outcome = TextIO.inputLine childin
   2.398  	   val probfile = TextIO.inputLine childin
   2.399 -	   val sg_num = number_from_filename probfile
   2.400 -	   val text = string_of_subgoal th sg_num
   2.401 +	   val sgno = number_from_filename probfile
   2.402 +	   val text = string_of_subgoal th sgno
   2.403  	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
   2.404  		        "\"\nprobfile = " ^ probfile ^
   2.405 -		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
   2.406 +		        "\nGoals being watched: "^  Int.toString (!goals_being_watched))
   2.407         in 
   2.408  	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
   2.409  	 then (priority (Recon_Transfer.apply_res_thm outcome);
     3.1 --- a/src/HOL/Tools/res_atp.ML	Thu Oct 06 10:14:22 2005 +0200
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Oct 07 11:29:24 2005 +0200
     3.3 @@ -176,17 +176,11 @@
     3.4    if Thm.no_prems th then ()
     3.5    else
     3.6      let
     3.7 -      fun reap s = (*Signal handler to tidy away dead processes*)
     3.8 -	   (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
     3.9 -		SOME _ => reap s | NONE => ()) 
    3.10 -           handle OS.SysErr _ => ()
    3.11 -      val _ = 
    3.12 -	      IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)
    3.13        val _ = (case !last_watcher_pid of NONE => ()
    3.14                 | SOME (_, childout, pid, files) => 
    3.15                    (debug ("Killing old watcher, pid = " ^ 
    3.16                            Int.toString (ResLib.intOfPid pid));
    3.17 -                   Watcher.killWatcher pid;
    3.18 +                   Watcher.killWatcher pid;  
    3.19                     ignore (map (try OS.FileSys.remove) files)))
    3.20                handle OS.SysErr _ => debug "Attempt to kill watcher failed";
    3.21        val (files,clause_arr) = write_problem_files prob_pathname (ctxt,th)