src/HOL/Tools/ATP/watcher.ML
author paulson
Wed Sep 28 11:16:27 2005 +0200 (2005-09-28)
changeset 17690 8ba7c3cd24a8
parent 17583 c272b91b619f
child 17716 89932e53f31d
permissions -rw-r--r--
time limit option; fixed bug concerning first line of ATP output
     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 fun prems_string_of th =
   224   Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
   225 
   226 fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
   227 
   228 fun killChildren procs = List.app (ignore o killChild) procs;
   229 
   230  (*************************************************************)
   231  (* take an instream and poll its underlying reader for input *)
   232  (*************************************************************)
   233  
   234  fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = 
   235    case OS.IO.pollDesc fromParentIOD of
   236       SOME pd =>
   237 	 (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
   238 	      [] => NONE
   239 	    | pd''::_ => if OS.IO.isIn pd''
   240 	 	         then SOME (getCmds (toParentStr, fromParentStr, []))
   241 	 	         else NONE)
   242    | NONE => NONE;
   243 
   244 (*get the number of the subgoal from the filename: the last digit string*)
   245 fun number_from_filename s =
   246   case String.tokens (not o Char.isDigit) s of
   247       [] => (trace "\nWatcher could not read subgoal nunber!!"; raise ERROR)
   248     | numbers => valOf (Int.fromString (List.last numbers));
   249 
   250 fun setupWatcher (thm,clause_arr) = 
   251   let
   252     (** pipes for communication between parent and watcher **)
   253     val p1 = Posix.IO.pipe ()
   254     val p2 = Posix.IO.pipe ()
   255     fun closep () = 
   256 	 (Posix.IO.close (#outfd p1); 
   257 	  Posix.IO.close (#infd p1);
   258 	  Posix.IO.close (#outfd p2); 
   259 	  Posix.IO.close (#infd p2))
   260     (***********************************************************)
   261     (****** fork a watcher process and get it set up and going *)
   262     (***********************************************************)
   263     fun startWatcher procList =
   264      (case  Posix.Process.fork() (***************************************)
   265       of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   266 				    (***************************************)
   267 
   268 				      (*************************)
   269        | NONE => let                  (* child - i.e. watcher  *)
   270 	  val oldchildin = #infd p1   (*************************)
   271 	  val fromParent = Posix.FileSys.wordToFD 0w0
   272 	  val oldchildout = #outfd p2
   273 	  val toParent = Posix.FileSys.wordToFD 0w1
   274 	  val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   275 	  val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   276 	  val toParentStr = openOutFD ("_exec_out_parent", toParent)
   277 	  val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   278 	 
   279 	  fun pollChildInput fromStr = 
   280 	     case getInIoDesc fromStr of
   281 	       SOME iod => 
   282 		 (case OS.IO.pollDesc iod of
   283 		    SOME pd =>
   284 			let val pd' = OS.IO.pollIn pd
   285 			in
   286 			  case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
   287 			      [] => false
   288 			    | pd''::_ => OS.IO.isIn pd''
   289 			end
   290 		   | NONE => false)
   291 	     | NONE => false
   292 
   293 
   294 	  (* Check all ATP processes currently running for output                 *)
   295 	  fun checkChildren ([], toParentStr) = []  (* no children to check *)
   296 	  |   checkChildren (childProc::otherChildren, toParentStr) = 
   297 	       let val _ = trace ("\nIn check child, length of queue:"^
   298 			          Int.toString (length (childProc::otherChildren)))
   299 		   val (childInput,childOutput) = cmdstreamsOf childProc
   300 		   val child_handle = cmdchildHandle childProc
   301 		   (* childCmd is the file that the problem is in *)
   302 		   val childCmd = fst(snd (cmdchildInfo childProc))
   303 		   val _ = trace ("\nchildCmd = " ^ childCmd)
   304 		   val sg_num = number_from_filename childCmd
   305 		   val childIncoming = pollChildInput childInput
   306 		   val parentID = Posix.ProcEnv.getppid()
   307 		   val prover = cmdProver childProc
   308 		   val prems_string = prems_string_of thm
   309 		   val goalstring = cmdGoal childProc							
   310 	       in 
   311 		 trace("\nsubgoals forked to checkChildren: " ^ goalstring);
   312 		 if childIncoming
   313 		 then 
   314 		   (* check here for prover label on child*)
   315 		   let val _ = trace ("\nInput available from child: " ^
   316 				      childCmd ^ 
   317 				      "\ngoalstring is " ^ goalstring ^ "\n\n")
   318 		       val childDone = (case prover of
   319 			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
   320 			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
   321 			  |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  )
   322 		    in
   323 		     if childDone
   324 		     then (* child has found a proof and transferred it *)
   325 			(* Remove this child and go on to check others*)
   326 			(Unix.reap child_handle;
   327 			 checkChildren(otherChildren, toParentStr))
   328 		     else (* Keep this child and go on to check others  *)
   329 		       childProc :: checkChildren (otherChildren, toParentStr)
   330 		  end
   331 		else (trace "\nNo child output";
   332 		      childProc::(checkChildren (otherChildren, toParentStr)))
   333 	       end
   334 
   335 	
   336      (********************************************************************)                  
   337      (* call resolution processes                                        *)
   338      (* settings should be a list of strings                             *)
   339      (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
   340      (* takes list of (string, string, string list, string)list proclist *)
   341      (********************************************************************)
   342 
   343 
   344 (*** add subgoal id num to this *)
   345 	fun execCmds  [] procList = procList
   346 	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   347 	      let val _ = trace 
   348 	                    (space_implode "\n" 
   349 	                      (["\nAbout to execute command for goal:",
   350 	                        goalstring, proverCmd] @ settings @
   351 	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   352 	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   353 		       (Unix.execute(proverCmd, (settings@[file])))
   354 		  val (instr, outstr) = Unix.streamsOf childhandle
   355 		  val newProcList = (CMDPROC{
   356 				       prover = prover,
   357 				       cmd = file,
   358 				       goalstring = goalstring,
   359 				       proc_handle = childhandle,
   360 				       instr = instr,
   361 				       outstr = outstr }) :: procList
   362      
   363 		  val _ = trace ("\nFinished at " ^
   364 			         Date.toString(Date.fromTimeLocal(Time.now())))
   365 	      in execCmds cmds newProcList end
   366 
   367 
   368      (****************************************)                  
   369      (* call resolution processes remotely   *)
   370      (* settings should be a list of strings *)
   371      (* e.g. ["-t300", "-m100000"]         *)
   372      (****************************************)
   373 
   374       (*  fun execRemoteCmds  [] procList = procList
   375 	|   execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList  =  
   376 	      let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   377 		  in
   378 		       execRemoteCmds  cmds newProcList
   379 		  end
   380 *)
   381 
   382      (**********************************************)                  
   383      (* Watcher Loop                               *)
   384      (**********************************************)
   385          val iterations_left = ref 500;  (*don't let it run forever*)
   386 
   387 	 fun keepWatching (procList) = 
   388 	   let fun loop procList =  
   389 		let val _ = trace ("\nCalling pollParentInput: " ^ 
   390 			           Int.toString (!iterations_left));
   391 		    val cmdsFromIsa = pollParentInput 
   392 		                       (fromParentIOD, fromParentStr, toParentStr)
   393 		in 
   394 		   OS.Process.sleep (Time.fromMilliseconds 100);
   395 		   iterations_left := !iterations_left - 1;
   396 		   if !iterations_left <= 0 
   397 		   then 
   398 		    (trace "\nTimeout: Killing proof processes";
   399 	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   400 		     TextIO.flushOut toParentStr;
   401 		     killChildren (map cmdchildHandle procList);
   402 		     exit 0)
   403 		   else if isSome cmdsFromIsa
   404 		   then (*  deal with input from Isabelle *)
   405 		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
   406 		     then 
   407 		       let val child_handles = map cmdchildHandle procList 
   408 		       in
   409 			  killChildren child_handles;
   410 			  loop []
   411 		       end
   412 		     else
   413 		       if length procList < 5     (********************)
   414 		       then                        (* Execute locally  *)
   415 			 let 
   416 			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   417 			   val _ = Posix.ProcEnv.getppid()
   418 			   val _ = trace "\nJust execed a child"
   419 			   val newProcList' = checkChildren (newProcList, toParentStr) 
   420 			 in
   421 			   trace ("\nOff to keep watching: " ^ 
   422 			          Int.toString (!iterations_left));
   423 			   loop newProcList'
   424 			 end
   425 		       else  (* Execute remotely              *)
   426 			     (* (actually not remote for now )*)
   427 			 let 
   428 			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   429 			   val _ = Posix.ProcEnv.getppid()
   430 			   val newProcList' =checkChildren (newProcList, toParentStr) 
   431 			 in
   432 			   loop newProcList'
   433 			 end
   434 		   else (* No new input from Isabelle *)
   435 		     let val newProcList = checkChildren (procList, toParentStr)
   436 		     in
   437 		       trace ("\nNo new input, still watching: " ^ 
   438 			      Int.toString (!iterations_left));
   439 		       loop newProcList
   440 		     end
   441 		 end
   442 	   in  
   443 	       loop procList
   444 	   end
   445 	   
   446 
   447 	   in
   448 	    (***************************)
   449 	    (*** Sort out pipes ********)
   450 	    (***************************)
   451 
   452 	     Posix.IO.close (#outfd p1);
   453 	     Posix.IO.close (#infd p2);
   454 	     Posix.IO.dup2{old = oldchildin, new = fromParent};
   455 	     Posix.IO.close oldchildin;
   456 	     Posix.IO.dup2{old = oldchildout, new = toParent};
   457 	     Posix.IO.close oldchildout;
   458 
   459 	     (***************************)
   460 	     (* start the watcher loop  *)
   461 	     (***************************)
   462 	     keepWatching (procList);
   463 	     (****************************************************************************)
   464 (* fake return value - actually want the watcher to loop until killed *)
   465 	     (****************************************************************************)
   466 	     Posix.Process.wordToPid 0w0
   467 	   end);
   468      (* end case *)
   469 
   470 
   471     val _ = TextIO.flushOut TextIO.stdOut
   472 
   473     (*******************************)
   474     (***  set watcher going ********)
   475     (*******************************)
   476 
   477     val procList = []
   478     val pid = startWatcher procList
   479     (**************************************************)
   480     (* communication streams to watcher               *)
   481     (**************************************************)
   482 
   483     val instr = openInFD ("_exec_in", #infd p2)
   484     val outstr = openOutFD ("_exec_out", #outfd p1)
   485     
   486   in
   487    (*******************************)
   488    (* close the child-side fds    *)
   489    (*******************************)
   490     Posix.IO.close (#outfd p2);
   491     Posix.IO.close (#infd p1);
   492     (* set the fds close on exec *)
   493     Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   494     Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   495      
   496    (*******************************)
   497    (* return value                *)
   498    (*******************************)
   499     PROC{pid = pid, instr = instr, outstr = outstr}
   500   end;
   501 
   502 
   503 
   504 (**********************************************************)
   505 (* Start a watcher and set up signal handlers             *)
   506 (**********************************************************)
   507 
   508 fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   509 
   510 val killWatcher' = killWatcher o ResLib.pidOfInt;
   511 
   512 fun reapWatcher(pid, instr, outstr) =
   513   (TextIO.closeIn instr; TextIO.closeOut outstr;
   514    Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
   515 
   516 fun createWatcher (thm, clause_arr) =
   517  let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
   518      fun decr_watched() =
   519 	  (goals_being_watched := !goals_being_watched - 1;
   520 	   if !goals_being_watched = 0
   521 	   then 
   522 	     (trace ("\nReaping a watcher, childpid = "^
   523 		     LargeWord.toString (Posix.Process.pidToWord childpid));
   524 	      killWatcher childpid; reapWatcher (childpid,childin, childout))
   525 	    else ())
   526      val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
   527      fun proofHandler n = 
   528        let val outcome = TextIO.inputLine childin
   529 	   val goalstring = TextIO.inputLine childin
   530 	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
   531 		        "\"\ngoalstring = " ^ goalstring ^
   532 		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
   533        in 
   534 	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
   535 	 then (priority (Recon_Transfer.apply_res_thm outcome goalstring);
   536 	       decr_watched())
   537 	 else if String.isPrefix "Invalid" outcome
   538 	 then (priority (goalstring ^ "is not provable");
   539 	       decr_watched())
   540 	 else if String.isPrefix "Failure" outcome
   541 	 then (priority (goalstring ^ "proof attempt failed");
   542 	       decr_watched()) 
   543 	(* print out a list of rules used from clasimpset*)
   544 	 else if String.isPrefix "Success" outcome
   545 	 then (priority (goalstring^outcome);
   546 	       decr_watched())
   547 	  (* if proof translation failed *)
   548 	 else if String.isPrefix "Translation failed" outcome
   549 	 then (priority (goalstring ^ outcome);
   550 	       decr_watched())
   551 	 else (priority "System error in proof handler";
   552 	       decr_watched())
   553        end
   554  in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
   555     (childin, childout, childpid)
   556   end
   557 
   558 end (* structure Watcher *)