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