src/HOL/Tools/ATP/watcher.ML
author paulson
Thu Sep 22 14:09:48 2005 +0200 (2005-09-22)
changeset 17583 c272b91b619f
parent 17568 e93f7510e1e1
child 17690 8ba7c3cd24a8
permissions -rw-r--r--
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
     1 (*  Title:      Watcher.ML
     2     ID:         $Id$
     3     Author:     Claire Quigley
     4     Copyright   2004  University of Cambridge
     5  *)
     6 
     7  (***************************************************************************)
     8  (*  The watcher process starts a resolution process when it receives a     *)
     9 (*  message from Isabelle                                                  *)
    10 (*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    11 (*  and removes dead processes.  Also possible to kill all the resolution  *)
    12 (*  processes currently running.                                           *)
    13 (*  Hardwired version of where to pick up the tptp files for the moment    *)
    14 (***************************************************************************)
    15 
    16 signature WATCHER =
    17 sig
    18 
    19 (*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
    20 (* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
    21 
    22 val callResProvers :
    23     TextIO.outstream * (string*string*string*string*string) list 
    24     -> unit
    25 
    26 (* Send message to watcher to kill currently running resolution provers *)
    27 val callSlayer : TextIO.outstream -> unit
    28 
    29 (* Start a watcher and set up signal handlers             *)
    30 val createWatcher : 
    31     thm * (ResClause.clause * thm) Array.array -> 
    32     TextIO.instream * TextIO.outstream * Posix.Process.pid
    33 
    34 (* Kill watcher process                                   *)
    35 val killWatcher : Posix.Process.pid -> unit
    36 val killWatcher' : int -> unit
    37 end
    38 
    39 
    40 
    41 structure Watcher: WATCHER =
    42 struct
    43 
    44 open Recon_Transfer
    45 
    46 val goals_being_watched = ref 0;
    47 
    48 val trace_path = Path.basic "watcher_trace";
    49 
    50 
    51 (*  The result of calling createWatcher  *)
    52 datatype proc = PROC of {
    53         pid : Posix.Process.pid,
    54         instr : TextIO.instream,
    55         outstr : TextIO.outstream
    56       };
    57 
    58 (*  The result of calling executeToList  *)
    59 datatype cmdproc = CMDPROC of {
    60         prover: string,       (* Name of the resolution prover used, e.g. Vampire*)
    61         cmd:  string,         (* The file containing the goal for res prover to prove *)     
    62         goalstring: string,   (* string representation of subgoal*) 
    63         proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    64         instr : TextIO.instream,   (*  Input stream to child process *)
    65         outstr : TextIO.outstream};  (*  Output stream from child process *)
    66 
    67 type signal = Posix.Signal.signal
    68 datatype exit_status = datatype Posix.Process.exit_status
    69 
    70 val fromStatus = Posix.Process.fromStatus
    71 
    72 fun reap(pid, instr, outstr) =
    73   let val u = TextIO.closeIn instr;
    74       val u = TextIO.closeOut outstr;
    75       val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    76   in status end
    77 
    78 fun fdReader (name : string, fd : Posix.IO.file_desc) =
    79 	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    80 
    81 fun fdWriter (name, fd) =
    82           Posix.IO.mkTextWriter {
    83 	      appendMode = false,
    84               initBlkMode = true,
    85               name = name,  
    86               chunkSize=4096,
    87               fd = fd};
    88 
    89 fun openOutFD (name, fd) =
    90 	  TextIO.mkOutstream (
    91 	    TextIO.StreamIO.mkOutstream (
    92 	      fdWriter (name, fd), IO.BLOCK_BUF));
    93 
    94 fun openInFD (name, fd) =
    95 	  TextIO.mkInstream (
    96 	    TextIO.StreamIO.mkInstream (
    97 	      fdReader (name, fd), ""));
    98 
    99 fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
   100 
   101 fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
   102 
   103 fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
   104 
   105 fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) = 
   106   (prover,(cmd, (instr,outstr)));
   107 
   108 fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  = 
   109   proc_handle;
   110 
   111 fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
   112   prover;
   113 
   114 fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
   115   goalstring;
   116 
   117 
   118 (*    gets individual args from instream and concatenates them into a list      *)
   119 fun getArgs (fromParentStr, toParentStr, ys) =  
   120   let val thisLine = TextIO.input fromParentStr
   121   in ys@[thisLine] end
   122 
   123                             
   124 (*  Send request to Watcher for a vampire to be called for filename in arg      *)
   125                    
   126 fun callResProver (toWatcherStr,  arg) = 
   127       (TextIO.output (toWatcherStr, arg^"\n"); 
   128        TextIO.flushOut toWatcherStr)
   129 
   130 (*****************************************************************************************)
   131 (*  Send request to Watcher for multiple provers to be called for filenames in arg       *)
   132 (*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
   133 (*****************************************************************************************)
   134 
   135     
   136 (*Uses the $-character to separate items sent to watcher*)
   137 fun callResProvers (toWatcherStr,  []) = 
   138       (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
   139 |   callResProvers (toWatcherStr,
   140                     (prover,goalstring, proverCmd,settings, 
   141                      probfile)  ::  args) =
   142       let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
   143                              (prover^goalstring^proverCmd^settings^
   144                               probfile)
   145       in TextIO.output (toWatcherStr,    
   146             (prover^"$"^goalstring^"$"^proverCmd^"$"^
   147              settings^"$"^probfile^"\n"));
   148          goals_being_watched := (!goals_being_watched) + 1;
   149 	 TextIO.flushOut toWatcherStr;
   150 	 callResProvers (toWatcherStr,args)
   151       end   
   152                                                 
   153                                     
   154  
   155 (**************************************************************)
   156 (* Send message to watcher to kill currently running vampires *)
   157 (**************************************************************)
   158 
   159 fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n"); 
   160                             TextIO.flushOut toWatcherStr)
   161 
   162 
   163 
   164 (**************************************************************)
   165 (* Remove \n token from a vampire goal filename and extract   *)
   166 (* prover, proverCmd, settings and file from input string     *)
   167 (**************************************************************)
   168 
   169 fun separateFields str =
   170   let val _ = File.append (File.tmp_path (Path.basic "sep_field"))
   171                           ("In separateFields, str is: " ^ str ^ "\n\n") 
   172       val [prover,goalstring,proverCmd,settingstr,probfile] = 
   173           String.tokens (fn c => c = #"$") str
   174       val settings = String.tokens (fn c => c = #"%") settingstr
   175       val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
   176                   ("Sep comms are: "^ str ^"**"^
   177                    prover^" goalstr:  "^goalstring^
   178                    "\n provercmd: "^proverCmd^
   179                    "\n prob  "^probfile^"\n\n")
   180   in
   181      (prover,goalstring, proverCmd, settings, probfile)
   182   end
   183 
   184 val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
   185 
   186 fun getCmd cmdStr = 
   187   let val cmdStr' = remove_newlines cmdStr
   188   in
   189       File.write (File.tmp_path (Path.basic"sepfields_call")) 
   190 		 ("about to call separateFields with " ^ cmdStr');
   191       separateFields cmdStr'
   192   end;
   193                       
   194 (**************************************************************)
   195 (* Get commands from Isabelle                                 *)
   196 (**************************************************************)
   197 
   198 fun getCmds (toParentStr,fromParentStr, cmdList) = 
   199   let val thisLine = TextIO.inputLine fromParentStr 
   200       val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
   201   in
   202      if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
   203      else if thisLine = "Kill children\n"
   204      then (TextIO.output (toParentStr,thisLine ); 
   205 	   TextIO.flushOut toParentStr;
   206 	   (("","","Kill children",[],"")::cmdList)  )
   207      else let val thisCmd = getCmd thisLine 
   208 	       (*********************************************************)
   209 	       (* thisCmd = (prover,proverCmd, settings, file)*)
   210 	       (* i.e. put back into tuple format                       *)
   211 	       (*********************************************************)
   212 	   in
   213 	       getCmds (toParentStr, fromParentStr, thisCmd::cmdList)
   214 	   end
   215   end
   216 	    
   217                                                                   
   218 (**************************************************************)
   219 (*  Get Io-descriptor for polling of an input stream          *)
   220 (**************************************************************)
   221 
   222 fun getInIoDesc someInstr = 
   223     let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   224         val _ = TextIO.output (TextIO.stdOut, buf)
   225         val ioDesc = 
   226 	    case rd
   227 	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
   228 	       | _ => NONE
   229      in (* since getting the reader will have terminated the stream, we need
   230 	 * to build a new stream. *)
   231 	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
   232 	ioDesc
   233     end
   234 
   235 
   236 (*************************************)
   237 (*  Set up a Watcher Process         *)
   238 (*************************************)
   239 
   240 fun getProofCmd (a,c,d,e,f) = d
   241 
   242 fun prems_string_of th =
   243   Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
   244 
   245 fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
   246 
   247 fun killChildren procs = List.app (ignore o killChild) procs;
   248 
   249  (*************************************************************)
   250  (* take an instream and poll its underlying reader for input *)
   251  (*************************************************************)
   252  
   253  fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = 
   254    case OS.IO.pollDesc fromParentIOD
   255    of SOME pd =>
   256        let val pd' = OS.IO.pollIn pd
   257 	   val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   258        in
   259 	  if null pdl 
   260 	  then NONE
   261 	  else if OS.IO.isIn (hd pdl)
   262 	       then SOME (getCmds (toParentStr, fromParentStr, []))
   263 	       else NONE
   264        end
   265    | NONE => NONE;
   266 
   267 (*get the number of the subgoal from the filename: the last digit string*)
   268 fun number_from_filename s =
   269   case String.tokens (not o Char.isDigit) s of
   270       [] => (File.append (File.tmp_path trace_path) 
   271 		    "\nWatcher could not read subgoal nunber!!";
   272 		    raise ERROR)
   273     | numbers => valOf (Int.fromString (List.last numbers));
   274 
   275 fun setupWatcher (thm,clause_arr) = 
   276   let
   277     (** pipes for communication between parent and watcher **)
   278     val p1 = Posix.IO.pipe ()
   279     val p2 = Posix.IO.pipe ()
   280     fun closep () = 
   281 	 (Posix.IO.close (#outfd p1); 
   282 	  Posix.IO.close (#infd p1);
   283 	  Posix.IO.close (#outfd p2); 
   284 	  Posix.IO.close (#infd p2))
   285     (***********************************************************)
   286     (****** fork a watcher process and get it set up and going *)
   287     (***********************************************************)
   288     fun startWatcher procList =
   289      (case  Posix.Process.fork() (***************************************)
   290       of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   291 				    (***************************************)
   292 
   293 				      (*************************)
   294        | NONE => let                  (* child - i.e. watcher  *)
   295 	   val oldchildin = #infd p1  (*************************)
   296 	   val fromParent = Posix.FileSys.wordToFD 0w0
   297 	   val oldchildout = #outfd p2
   298 	   val toParent = Posix.FileSys.wordToFD 0w1
   299 	   val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   300 	   val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   301 	   val toParentStr = openOutFD ("_exec_out_parent", toParent)
   302 	   val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   303 	 
   304 	  fun pollChildInput fromStr = 
   305 	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
   306 			 ("\nIn child_poll")
   307 	       val iod = getInIoDesc fromStr
   308 	   in 
   309 	     if isSome iod 
   310 	     then 
   311 	       let val pd = OS.IO.pollDesc (valOf iod)
   312 	       in 
   313 	       if isSome pd then 
   314 		   let val pd' = OS.IO.pollIn (valOf pd)
   315 		       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   316 		   in
   317 		      if null pdl 
   318 		      then
   319 			(File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl\n"; 
   320 			 NONE)
   321 		      else if OS.IO.isIn (hd pdl)
   322 		      then
   323 			   let val inval = TextIO.inputLine fromStr
   324 			       val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
   325 			   in SOME inval end
   326 		      else
   327                         (File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl \n";
   328                          NONE)
   329 		   end
   330 		 else NONE
   331 		 end
   332 	     else NONE
   333 	   end
   334 
   335 	(* Check all ATP processes currently running for output                 *)
   336 						   (*********************************)
   337 	 fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   338 						   (*********************************)
   339 	 |   checkChildren ((childProc::otherChildren), toParentStr) = 
   340 	       let val _ = File.append (File.tmp_path trace_path) 
   341 			      ("\nIn check child, length of queue:"^
   342 			        Int.toString (length (childProc::otherChildren)))
   343 		   val (childInput,childOutput) = cmdstreamsOf childProc
   344 		   val child_handle = cmdchildHandle childProc
   345 		   (* childCmd is the .dfg file that the problem is in *)
   346 		   val childCmd = fst(snd (cmdchildInfo childProc))
   347 		   val _ = File.append (File.tmp_path trace_path) 
   348 			      ("\nchildCmd = " ^ childCmd)
   349 		   val sg_num = number_from_filename childCmd
   350 		   val childIncoming = pollChildInput childInput
   351 		   val _ = File.append (File.tmp_path trace_path) 
   352 			         "\nfinished polling child"
   353 		   val parentID = Posix.ProcEnv.getppid()
   354 		   val prover = cmdProver childProc
   355 		   val prems_string = prems_string_of thm
   356 		   val goalstring = cmdGoal childProc							
   357 		   val _ =  File.append (File.tmp_path trace_path) 
   358 		             ("\nsubgoals forked to checkChildren: " ^ goalstring)
   359 	       in 
   360 		 if isSome childIncoming
   361 		 then 
   362 		   (* check here for prover label on child*)
   363 		   let val _ = File.append (File.tmp_path trace_path) 
   364 			        ("\nInput available from childIncoming" ^
   365 			         "\nchecking if proof found." ^
   366 			         "\nchildCmd is " ^ childCmd ^ 
   367 			         "\ngoalstring is: " ^ goalstring ^ "\n\n")
   368 		       val childDone = (case prover of
   369 			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
   370 			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
   371 			  |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  )
   372 		    in
   373 		     if childDone
   374 		     then (* child has found a proof and transferred it *)
   375 			(* Remove this child and go on to check others*)
   376 			(**********************************************)
   377 			(Unix.reap child_handle;
   378 			 checkChildren(otherChildren, toParentStr))
   379 		     else 
   380 			(**********************************************)
   381 			(* Keep this child and go on to check others  *)
   382 			(**********************************************)
   383 		       (childProc::(checkChildren (otherChildren, toParentStr)))
   384 		  end
   385 		else
   386 		  (File.append (File.tmp_path trace_path)
   387 		               "\nNo child output";
   388 		   childProc::(checkChildren (otherChildren, toParentStr)))
   389 	       end
   390 
   391 	
   392      (********************************************************************)                  
   393      (* call resolution processes                                        *)
   394      (* settings should be a list of strings                             *)
   395      (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
   396      (* takes list of (string, string, string list, string)list proclist *)
   397      (********************************************************************)
   398 
   399 
   400 (*** add subgoal id num to this *)
   401 	fun execCmds  [] procList = procList
   402 	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   403 	      let val _ = File.write (File.tmp_path (Path.basic "exec_child"))  
   404 	                    (space_implode "\n" 
   405 	                      (["About to execute command for goal:",
   406 	                        goalstring, proverCmd] @ settings @
   407 	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   408 	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   409 		       (Unix.execute(proverCmd, (settings@[file])))
   410 		  val (instr, outstr) = Unix.streamsOf childhandle
   411 		  
   412 		  val newProcList = (CMDPROC{
   413 				       prover = prover,
   414 				       cmd = file,
   415 				       goalstring = goalstring,
   416 				       proc_handle = childhandle,
   417 				       instr = instr,
   418 				       outstr = outstr }) :: procList
   419      
   420 		  val _ = File.append (File.tmp_path (Path.basic "exec_child")) 
   421 			    ("\nFinished at " ^
   422 			     Date.toString(Date.fromTimeLocal(Time.now())))
   423 	      in
   424 		execCmds cmds newProcList
   425 	      end
   426 
   427 
   428      (****************************************)                  
   429      (* call resolution processes remotely   *)
   430      (* settings should be a list of strings *)
   431      (* e.g. ["-t300", "-m100000"]         *)
   432      (****************************************)
   433 
   434       (*  fun execRemoteCmds  [] procList = procList
   435 	|   execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList  =  
   436 	      let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   437 		  in
   438 		       execRemoteCmds  cmds newProcList
   439 		  end
   440 *)
   441 
   442      (**********************************************)                  
   443      (* Watcher Loop                               *)
   444      (**********************************************)
   445          val iterations_left = ref 500;  (*don't let it run forever*)
   446 
   447 	 fun keepWatching (procList) = 
   448 	   let fun loop procList =  
   449 		let val _ = File.append (File.tmp_path trace_path) 
   450 			       ("\nCalling pollParentInput: " ^ 
   451 			        Int.toString (!iterations_left));
   452 		    val cmdsFromIsa = pollParentInput 
   453 		                       (fromParentIOD, fromParentStr, toParentStr)
   454 		in 
   455 		   iterations_left := !iterations_left - 1;
   456 		   if !iterations_left <= 0 
   457 		   then (*Sadly, this code fails to terminate the watcher!*)
   458 		    (File.append (File.tmp_path trace_path) 
   459 			         "\nTimeout: Killing proof processes";
   460 	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   461 		     TextIO.flushOut toParentStr;
   462 		     killChildren (map cmdchildHandle procList);
   463 		     exit 0)
   464 		   else if isSome cmdsFromIsa
   465 		   then (*  deal with input from Isabelle *)
   466 		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
   467 		     then 
   468 		       let val child_handles = map cmdchildHandle procList 
   469 		       in
   470 			  killChildren child_handles;
   471 			  loop []
   472 		       end
   473 		     else
   474 		       if length procList < 5     (********************)
   475 		       then                        (* Execute locally  *)
   476 			 let 
   477 			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   478 			   val _ = Posix.ProcEnv.getppid()
   479 			   val _ = File.append (File.tmp_path trace_path)
   480 			      "\nJust execed a child"
   481 			   val newProcList' = checkChildren (newProcList, toParentStr) 
   482 			 in
   483 			   File.append (File.tmp_path trace_path) 
   484 			       ("\nOff to keep watching: " ^ 
   485 			        Int.toString (!iterations_left));
   486 			   loop newProcList'
   487 			 end
   488 		       else  (* Execute remotely              *)
   489 			     (* (actually not remote for now )*)
   490 			 let 
   491 			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   492 			   val _ = Posix.ProcEnv.getppid()
   493 			   val newProcList' =checkChildren (newProcList, toParentStr) 
   494 			 in
   495 			   loop newProcList'
   496 			 end
   497 		   else (* No new input from Isabelle *)
   498 		     let val newProcList = checkChildren (procList, toParentStr)
   499 		     in
   500 		       File.append (File.tmp_path trace_path) 
   501 			       ("\nNo new input, still watching: " ^ 
   502 			        Int.toString (!iterations_left));
   503 		       loop newProcList
   504 		     end
   505 		 end
   506 	   in  
   507 	       loop procList
   508 	   end
   509 	   
   510 
   511 	   in
   512 	    (***************************)
   513 	    (*** Sort out pipes ********)
   514 	    (***************************)
   515 
   516 	     Posix.IO.close (#outfd p1);
   517 	     Posix.IO.close (#infd p2);
   518 	     Posix.IO.dup2{old = oldchildin, new = fromParent};
   519 	     Posix.IO.close oldchildin;
   520 	     Posix.IO.dup2{old = oldchildout, new = toParent};
   521 	     Posix.IO.close oldchildout;
   522 
   523 	     (***************************)
   524 	     (* start the watcher loop  *)
   525 	     (***************************)
   526 	     keepWatching (procList);
   527 	     (****************************************************************************)
   528 (* fake return value - actually want the watcher to loop until killed *)
   529 	     (****************************************************************************)
   530 	     Posix.Process.wordToPid 0w0
   531 	   end);
   532      (* end case *)
   533 
   534 
   535     val _ = TextIO.flushOut TextIO.stdOut
   536 
   537     (*******************************)
   538     (***  set watcher going ********)
   539     (*******************************)
   540 
   541     val procList = []
   542     val pid = startWatcher procList
   543     (**************************************************)
   544     (* communication streams to watcher               *)
   545     (**************************************************)
   546 
   547     val instr = openInFD ("_exec_in", #infd p2)
   548     val outstr = openOutFD ("_exec_out", #outfd p1)
   549     
   550   in
   551    (*******************************)
   552    (* close the child-side fds    *)
   553    (*******************************)
   554     Posix.IO.close (#outfd p2);
   555     Posix.IO.close (#infd p1);
   556     (* set the fds close on exec *)
   557     Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   558     Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   559      
   560    (*******************************)
   561    (* return value                *)
   562    (*******************************)
   563     PROC{pid = pid, instr = instr, outstr = outstr}
   564   end;
   565 
   566 
   567 
   568 (**********************************************************)
   569 (* Start a watcher and set up signal handlers             *)
   570 (**********************************************************)
   571 
   572 fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   573 
   574 val killWatcher' = killWatcher o ResLib.pidOfInt;
   575 
   576 fun reapWatcher(pid, instr, outstr) =
   577   (TextIO.closeIn instr; TextIO.closeOut outstr;
   578    Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
   579 
   580 fun createWatcher (thm, clause_arr) =
   581  let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
   582      fun decr_watched() =
   583 	  (goals_being_watched := !goals_being_watched - 1;
   584 	   if !goals_being_watched = 0
   585 	   then 
   586 	     (File.append (File.tmp_path (Path.basic "reap_found"))
   587 	       ("Reaping a watcher, childpid = "^
   588 		LargeWord.toString (Posix.Process.pidToWord childpid)^"\n");
   589 	      killWatcher childpid; reapWatcher (childpid,childin, childout))
   590 	    else ())
   591      val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
   592      fun proofHandler n = 
   593        let val outcome = TextIO.inputLine childin
   594 	   val goalstring = TextIO.inputLine childin
   595 	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
   596 		        "\"\ngoalstring = " ^ goalstring ^
   597 		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
   598        in 
   599 	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
   600 	 then (tracing (Recon_Transfer.apply_res_thm outcome goalstring);
   601 	       decr_watched())
   602 	 else if String.isPrefix "Invalid" outcome
   603 	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "is not provable");
   604 	       decr_watched())
   605 	 else if String.isPrefix "Failure" outcome
   606 	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "proof attempt failed");
   607 	       decr_watched()) 
   608 	(* print out a list of rules used from clasimpset*)
   609 	 else if String.isPrefix "Success" outcome
   610 	 then (tracing (goalstring^outcome);
   611 	       decr_watched())
   612 	  (* if proof translation failed *)
   613 	 else if String.isPrefix "Translation failed" outcome
   614 	 then (tracing (goalstring ^ Recon_Transfer.restore_linebreaks outcome);
   615 	       decr_watched())
   616 	 else  
   617 	      (tracing "System error in proof handler";
   618 	       decr_watched())
   619        end
   620  in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
   621     (childin, childout, childpid)
   622   end
   623 
   624 end (* structure Watcher *)