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