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