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