src/HOL/Tools/ATP/watcher.ML
author paulson
Fri Oct 07 11:29:24 2005 +0200 (2005-10-07)
changeset 17773 a7258e1020b7
parent 17772 818cec5f82a4
child 17774 0ecfb66ea072
permissions -rw-r--r--
more tidying. Fixed process management bugs and race condition
paulson@15789
     1
(*  Title:      Watcher.ML
paulson@15789
     2
    ID:         $Id$
paulson@15789
     3
    Author:     Claire Quigley
paulson@15789
     4
    Copyright   2004  University of Cambridge
quigley@15642
     5
 *)
quigley@15642
     6
paulson@17764
     7
(*  The watcher process starts a resolution process when it receives a     *)
quigley@15642
     8
(*  message from Isabelle                                                  *)
quigley@15642
     9
(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
quigley@15642
    10
(*  and removes dead processes.  Also possible to kill all the resolution  *)
quigley@15642
    11
(*  processes currently running.                                           *)
quigley@15642
    12
paulson@17305
    13
signature WATCHER =
paulson@17305
    14
sig
paulson@17305
    15
paulson@17305
    16
(*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
paulson@17568
    17
(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
paulson@17305
    18
paulson@17773
    19
val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit
paulson@17305
    20
paulson@17764
    21
(* Send message to watcher to kill resolution provers *)
paulson@17305
    22
val callSlayer : TextIO.outstream -> unit
paulson@17305
    23
paulson@17305
    24
(* Start a watcher and set up signal handlers             *)
paulson@17484
    25
val createWatcher : 
paulson@17484
    26
    thm * (ResClause.clause * thm) Array.array -> 
paulson@17484
    27
    TextIO.instream * TextIO.outstream * Posix.Process.pid
paulson@17305
    28
val killWatcher : Posix.Process.pid -> unit
paulson@17764
    29
val setting_sep : char
paulson@17305
    30
end
paulson@17305
    31
paulson@17305
    32
quigley@15642
    33
quigley@15642
    34
structure Watcher: WATCHER =
paulson@17484
    35
struct
quigley@15642
    36
paulson@17764
    37
(*Field separators, used to pack items onto a text line*)
paulson@17764
    38
val command_sep = #"\t"
paulson@17764
    39
and setting_sep = #"%";
paulson@17764
    40
quigley@15642
    41
val goals_being_watched = ref 0;
quigley@15642
    42
paulson@17583
    43
val trace_path = Path.basic "watcher_trace";
paulson@17583
    44
paulson@17690
    45
fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
paulson@17690
    46
              else ();
paulson@17583
    47
paulson@17773
    48
(*Representation of a watcher process*)
paulson@17773
    49
type proc = {pid : Posix.Process.pid,
paulson@17773
    50
             instr : TextIO.instream,
paulson@17773
    51
             outstr : TextIO.outstream};
quigley@16039
    52
paulson@17773
    53
(*Representation of a child (ATP) process*)
paulson@17773
    54
type cmdproc = {
paulson@17773
    55
        prover: string,       (* Name of the resolution prover used, e.g. "spass"*)
paulson@17773
    56
        file:  string,        (* The file containing the goal for the ATP to prove *)     
quigley@16039
    57
        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
paulson@17773
    58
        instr : TextIO.instream,     (*Output of the child process *)
paulson@17773
    59
        outstr : TextIO.outstream};  (*Input to the child process *)
quigley@16039
    60
quigley@16039
    61
quigley@16039
    62
fun fdReader (name : string, fd : Posix.IO.file_desc) =
quigley@16039
    63
	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
quigley@16039
    64
quigley@16039
    65
fun fdWriter (name, fd) =
quigley@16039
    66
          Posix.IO.mkTextWriter {
quigley@16039
    67
	      appendMode = false,
quigley@16039
    68
              initBlkMode = true,
quigley@16039
    69
              name = name,  
quigley@16039
    70
              chunkSize=4096,
paulson@17317
    71
              fd = fd};
quigley@16039
    72
quigley@16039
    73
fun openOutFD (name, fd) =
quigley@16039
    74
	  TextIO.mkOutstream (
quigley@16039
    75
	    TextIO.StreamIO.mkOutstream (
quigley@16039
    76
	      fdWriter (name, fd), IO.BLOCK_BUF));
quigley@16039
    77
quigley@16039
    78
fun openInFD (name, fd) =
quigley@16039
    79
	  TextIO.mkInstream (
quigley@16039
    80
	    TextIO.StreamIO.mkInstream (
quigley@16039
    81
	      fdReader (name, fd), ""));
quigley@16039
    82
quigley@15642
    83
                            
paulson@17773
    84
(*  Send request to Watcher for a vampire to be called for filename in arg*)
paulson@17231
    85
fun callResProver (toWatcherStr,  arg) = 
paulson@17317
    86
      (TextIO.output (toWatcherStr, arg^"\n"); 
paulson@17231
    87
       TextIO.flushOut toWatcherStr)
quigley@15642
    88
paulson@17773
    89
(*  Send request to Watcher for multiple provers to be called*)
paulson@16475
    90
fun callResProvers (toWatcherStr,  []) = 
paulson@17317
    91
      (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
paulson@17773
    92
  | callResProvers (toWatcherStr,
paulson@17772
    93
                    (prover,proverCmd,settings,probfile)  ::  args) =
paulson@17773
    94
      (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile]));
paulson@17773
    95
       (*Uses a special character to separate items sent to watcher*)
paulson@17773
    96
       TextIO.output (toWatcherStr,
paulson@17773
    97
          space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
paulson@17773
    98
       goals_being_watched := (!goals_being_watched) + 1;
paulson@17773
    99
       TextIO.flushOut toWatcherStr;
paulson@17773
   100
       callResProvers (toWatcherStr,args))
quigley@16357
   101
                                                
quigley@15642
   102
paulson@17764
   103
(*Send message to watcher to kill currently running vampires. NOT USED and possibly
paulson@17764
   104
  buggy. Note that killWatcher kills the entire process group anyway.*)
paulson@17764
   105
fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n"); 
quigley@15642
   106
                            TextIO.flushOut toWatcherStr)
quigley@15642
   107
paulson@17746
   108
                    
paulson@17773
   109
(* Get commands from Isabelle*)
paulson@17764
   110
fun getCmds (toParentStr, fromParentStr, cmdList) = 
paulson@16475
   111
  let val thisLine = TextIO.inputLine fromParentStr 
paulson@16475
   112
  in
paulson@17764
   113
     trace("\nGot command from parent: " ^ thisLine);
paulson@17568
   114
     if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
paulson@17422
   115
     else if thisLine = "Kill children\n"
paulson@17764
   116
     then (TextIO.output (toParentStr,thisLine); 
paulson@17568
   117
	   TextIO.flushOut toParentStr;
paulson@17772
   118
	   [("","Kill children",[],"")])
paulson@17746
   119
     else
paulson@17772
   120
       let val [prover,proverCmd,settingstr,probfile,_] = 
paulson@17764
   121
                   String.tokens (fn c => c = command_sep) thisLine
paulson@17764
   122
           val settings = String.tokens (fn c => c = setting_sep) settingstr
paulson@17746
   123
       in
paulson@17772
   124
           trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd ^
paulson@17772
   125
                  "\n  problem file: " ^ probfile);
paulson@17746
   126
           getCmds (toParentStr, fromParentStr, 
paulson@17772
   127
                    (prover, proverCmd, settings, probfile)::cmdList) 
paulson@17746
   128
       end
paulson@17764
   129
       handle Bind => 
paulson@17764
   130
          (trace "getCmds: command parsing failed!";
paulson@17764
   131
           getCmds (toParentStr, fromParentStr, cmdList))
paulson@16475
   132
  end
paulson@16475
   133
	    
quigley@16357
   134
                                                                  
quigley@15642
   135
(*  Get Io-descriptor for polling of an input stream          *)
quigley@15642
   136
fun getInIoDesc someInstr = 
quigley@15642
   137
    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
paulson@15702
   138
        val _ = TextIO.output (TextIO.stdOut, buf)
quigley@15642
   139
        val ioDesc = 
quigley@15642
   140
	    case rd
quigley@15642
   141
	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
quigley@15642
   142
	       | _ => NONE
quigley@15642
   143
     in (* since getting the reader will have terminated the stream, we need
quigley@15642
   144
	 * to build a new stream. *)
quigley@15642
   145
	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
quigley@15642
   146
	ioDesc
quigley@15642
   147
    end
quigley@15642
   148
quigley@15642
   149
quigley@15642
   150
(*************************************)
quigley@15642
   151
(*  Set up a Watcher Process         *)
quigley@15642
   152
(*************************************)
quigley@15642
   153
paulson@17525
   154
fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
paulson@17525
   155
paulson@17525
   156
fun killChildren procs = List.app (ignore o killChild) procs;
paulson@17502
   157
paulson@17568
   158
 (* take an instream and poll its underlying reader for input *)
paulson@17568
   159
 fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = 
paulson@17690
   160
   case OS.IO.pollDesc fromParentIOD of
paulson@17690
   161
      SOME pd =>
paulson@17690
   162
	 (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
paulson@17690
   163
	      [] => NONE
paulson@17690
   164
	    | pd''::_ => if OS.IO.isIn pd''
paulson@17690
   165
	 	         then SOME (getCmds (toParentStr, fromParentStr, []))
paulson@17690
   166
	 	         else NONE)
paulson@17568
   167
   | NONE => NONE;
paulson@17568
   168
paulson@17583
   169
(*get the number of the subgoal from the filename: the last digit string*)
paulson@17583
   170
fun number_from_filename s =
paulson@17583
   171
  case String.tokens (not o Char.isDigit) s of
paulson@17772
   172
      [] => (trace ("\nWatcher could not read subgoal nunber! " ^ s); 
paulson@17772
   173
             raise ERROR)
paulson@17583
   174
    | numbers => valOf (Int.fromString (List.last numbers));
paulson@17583
   175
paulson@17484
   176
fun setupWatcher (thm,clause_arr) = 
paulson@16061
   177
  let
paulson@17772
   178
    val p1 = Posix.IO.pipe()   (*pipes for communication between parent and watcher*)
paulson@17772
   179
    val p2 = Posix.IO.pipe()
paulson@17317
   180
    fun closep () = 
paulson@17764
   181
	 (Posix.IO.close (#outfd p1); Posix.IO.close (#infd p1);
paulson@17764
   182
	  Posix.IO.close (#outfd p2); Posix.IO.close (#infd p2))
paulson@17764
   183
    (****** fork a watcher process and get it set up and going ******)
paulson@17317
   184
    fun startWatcher procList =
paulson@17764
   185
     (case  Posix.Process.fork() 
paulson@17764
   186
      of SOME pid => pid (* parent - i.e. main Isabelle process *)
paulson@17764
   187
       | NONE => let                (* child - i.e. watcher  *)
paulson@17764
   188
	  val oldchildin = #infd p1  
paulson@17690
   189
	  val fromParent = Posix.FileSys.wordToFD 0w0
paulson@17690
   190
	  val oldchildout = #outfd p2
paulson@17690
   191
	  val toParent = Posix.FileSys.wordToFD 0w1
paulson@17690
   192
	  val fromParentIOD = Posix.FileSys.fdToIOD fromParent
paulson@17690
   193
	  val fromParentStr = openInFD ("_exec_in_parent", fromParent)
paulson@17690
   194
	  val toParentStr = openOutFD ("_exec_out_parent", toParent)
paulson@17764
   195
	  val pid = Posix.ProcEnv.getpid()
paulson@17764
   196
	  val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
paulson@17764
   197
                   (*set process group id: allows killing all children*)
paulson@17772
   198
	  val () = trace "\nsubgoals forked to startWatcher"
paulson@17773
   199
	  fun pollChild fromStr = 
paulson@17690
   200
	     case getInIoDesc fromStr of
paulson@17690
   201
	       SOME iod => 
paulson@17690
   202
		 (case OS.IO.pollDesc iod of
paulson@17690
   203
		    SOME pd =>
paulson@17764
   204
			let val pd' = OS.IO.pollIn pd in
paulson@17690
   205
			  case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
paulson@17690
   206
			      [] => false
paulson@17690
   207
			    | pd''::_ => OS.IO.isIn pd''
paulson@17690
   208
			end
paulson@17690
   209
		   | NONE => false)
paulson@17690
   210
	     | NONE => false
paulson@17690
   211
	  (* Check all ATP processes currently running for output                 *)
paulson@17690
   212
	  fun checkChildren ([], toParentStr) = []  (* no children to check *)
paulson@17690
   213
	  |   checkChildren (childProc::otherChildren, toParentStr) = 
paulson@17690
   214
	       let val _ = trace ("\nIn check child, length of queue:"^
paulson@17690
   215
			          Int.toString (length (childProc::otherChildren)))
paulson@17773
   216
		   val {prover, file, proc_handle, instr=childIn, ...} : cmdproc =
paulson@17773
   217
		       childProc
paulson@17773
   218
		   val _ = trace ("\nprobfile = " ^ file)
paulson@17773
   219
		   val sgno = number_from_filename file
paulson@17773
   220
		   val ppid = Posix.ProcEnv.getppid()
paulson@17234
   221
	       in 
paulson@17773
   222
		 if pollChild childIn
paulson@17764
   223
		 then (* check here for prover label on child*)
paulson@17773
   224
		   let val _ = trace ("\nInput available from child: " ^ file)
paulson@17306
   225
		       val childDone = (case prover of
paulson@17773
   226
			   "vampire" => AtpCommunication.checkVampProofFound
paulson@17773
   227
			        (childIn, toParentStr, ppid, file, clause_arr)  
paulson@17773
   228
		         | "E" => AtpCommunication.checkEProofFound
paulson@17773
   229
		                (childIn, toParentStr, ppid, file, clause_arr)             
paulson@17773
   230
			 | "spass" => AtpCommunication.checkSpassProofFound
paulson@17773
   231
			        (childIn, toParentStr, ppid, file, thm, sgno,clause_arr)  
paulson@17773
   232
			 | _ => (trace ("\nBad prover! " ^ prover); true) )
paulson@17306
   233
		    in
paulson@17773
   234
		     if childDone (*child has found a proof and transferred it*)
paulson@17773
   235
		     then (*Remove this child and go on to check others*)
paulson@17773
   236
		          (Unix.reap proc_handle; OS.FileSys.remove file;
paulson@17773
   237
			   checkChildren(otherChildren, toParentStr))
paulson@17690
   238
		     else (* Keep this child and go on to check others  *)
paulson@17690
   239
		       childProc :: checkChildren (otherChildren, toParentStr)
paulson@17306
   240
		  end
paulson@17690
   241
		else (trace "\nNo child output";
paulson@17690
   242
		      childProc::(checkChildren (otherChildren, toParentStr)))
paulson@17234
   243
	       end
paulson@17234
   244
	
paulson@17764
   245
	(* call resolution processes                                        *)
paulson@17773
   246
	(* settings should be a list of strings  ["-t300", "-m100000"]    *)
paulson@17764
   247
	fun execCmds [] procList = procList
paulson@17772
   248
	|   execCmds ((prover,proverCmd,settings,file)::cmds) procList  =
paulson@17773
   249
	      let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
paulson@17317
   250
	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
paulson@17764
   251
		       Unix.execute(proverCmd, settings@[file])
paulson@17234
   252
		  val (instr, outstr) = Unix.streamsOf childhandle
paulson@17773
   253
		  val newProcList = {prover = prover,
paulson@17773
   254
					    file = file,
paulson@17764
   255
					    proc_handle = childhandle,
paulson@17764
   256
					    instr = instr,
paulson@17764
   257
					    outstr = outstr} :: procList
paulson@17772
   258
     		  val _ = trace ("\nFinished at " ^
paulson@17690
   259
			         Date.toString(Date.fromTimeLocal(Time.now())))
paulson@17690
   260
	      in execCmds cmds newProcList end
quigley@15642
   261
paulson@17764
   262
         (******** Watcher Loop ********)
paulson@17772
   263
         val limit = ref 200;  (*don't let it run forever*)
paulson@16061
   264
paulson@17773
   265
	 fun keepWatching procList = 
paulson@17773
   266
	   let val _ = trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^ 
paulson@17773
   267
			      "  length(procList) = " ^ Int.toString (length procList));
paulson@17773
   268
	       val cmdsFromIsa = pollParentInput 
paulson@17773
   269
				  (fromParentIOD, fromParentStr, toParentStr)
paulson@17773
   270
	   in 
paulson@17773
   271
	     OS.Process.sleep (Time.fromMilliseconds 100);
paulson@17773
   272
	     limit := !limit - 1;
paulson@17773
   273
	     if !limit < 0 
paulson@17773
   274
	     then 
paulson@17773
   275
	      (trace "\nTimeout: Killing proof processes";
paulson@17773
   276
	       TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
paulson@17773
   277
	       TextIO.flushOut toParentStr;
paulson@17773
   278
	       killChildren (map #proc_handle procList);
paulson@17773
   279
	       Posix.Process.exit 0w0)
paulson@17773
   280
	     else 
paulson@17773
   281
	       case cmdsFromIsa of
paulson@17773
   282
		 SOME [(_,"Kill children",_,_)] => 
paulson@17773
   283
		   let val child_handles = map #proc_handle procList 
paulson@17773
   284
		   in  trace "\nReceived command to kill children";
paulson@17773
   285
		       killChildren child_handles; keepWatching [] 
paulson@17773
   286
		   end
paulson@17773
   287
	       | SOME cmds => (*  deal with commands from Isabelle process *)
paulson@17773
   288
		   if length procList < 40
paulson@17773
   289
		   then                        (* Execute locally  *)
paulson@17773
   290
		     let 
paulson@17773
   291
		       val _ = trace("\nCommands from parent: " ^ 
paulson@17773
   292
		                     Int.toString(length cmds))
paulson@17773
   293
		       val newProcList = execCmds cmds procList
paulson@17773
   294
		       val newProcList' = checkChildren (newProcList, toParentStr) 
paulson@17773
   295
		     in
paulson@17773
   296
		       trace "\nCommands executed"; keepWatching newProcList'
paulson@17773
   297
		     end
paulson@17773
   298
		   else  (* Execute remotely [FIXME: NOT REALLY]  *)
paulson@17773
   299
		     let 
paulson@17773
   300
		       val newProcList = execCmds cmds procList
paulson@17773
   301
		       val newProcList' = checkChildren (newProcList, toParentStr) 
paulson@17773
   302
		     in keepWatching newProcList' end
paulson@17773
   303
	       | NONE => (* No new input from Isabelle *)
paulson@17773
   304
		   let val newProcList = checkChildren (procList, toParentStr)
paulson@17773
   305
		   in trace "\nNothing from parent, still watching"; 
paulson@17773
   306
		      keepWatching newProcList
paulson@17773
   307
		   end
paulson@17773
   308
	   end
paulson@17773
   309
	   handle exn => (*FIXME: exn handler is too general!*)
paulson@17773
   310
	     (trace ("\nkeepWatching: In exception handler: " ^ Toplevel.exn_message exn);
paulson@17773
   311
	      keepWatching procList);
paulson@17764
   312
	 in
paulson@17772
   313
	   (*** Sort out pipes ********)
paulson@17772
   314
	   Posix.IO.close (#outfd p1);  Posix.IO.close (#infd p2);
paulson@17764
   315
	   Posix.IO.dup2{old = oldchildin, new = fromParent};
paulson@17764
   316
	   Posix.IO.close oldchildin;
paulson@17764
   317
	   Posix.IO.dup2{old = oldchildout, new = toParent};
paulson@17764
   318
	   Posix.IO.close oldchildout;
paulson@17772
   319
	   keepWatching (procList)
paulson@17772
   320
	 end);   (* end case *)
quigley@15642
   321
paulson@16061
   322
    val _ = TextIO.flushOut TextIO.stdOut
paulson@17772
   323
    val pid = startWatcher []
paulson@17772
   324
    (* communication streams to watcher*)
paulson@16061
   325
    val instr = openInFD ("_exec_in", #infd p2)
paulson@16061
   326
    val outstr = openOutFD ("_exec_out", #outfd p1)
paulson@17568
   327
  in
paulson@17772
   328
   (* close the child-side fds*)
paulson@17772
   329
    Posix.IO.close (#outfd p2);  Posix.IO.close (#infd p1);
paulson@17568
   330
    (* set the fds close on exec *)
paulson@17568
   331
    Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
paulson@17568
   332
    Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
paulson@17773
   333
    {pid = pid, instr = instr, outstr = outstr}
paulson@17568
   334
  end;
quigley@15642
   335
quigley@15642
   336
quigley@15642
   337
quigley@15642
   338
(**********************************************************)
quigley@15642
   339
(* Start a watcher and set up signal handlers             *)
quigley@15642
   340
(**********************************************************)
quigley@16039
   341
paulson@17773
   342
fun reapAll s = (*Signal handler to tidy away dead processes*)
paulson@17773
   343
     (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
paulson@17773
   344
	  SOME _ => reapAll s | NONE => ()) 
paulson@17773
   345
     handle OS.SysErr _ => ()
paulson@17773
   346
paulson@17773
   347
(*FIXME: does the main process need something like this?
paulson@17773
   348
    IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*)
paulson@17773
   349
paulson@17773
   350
fun killWatcher pid = 
paulson@17773
   351
  (goals_being_watched := 0;
paulson@17773
   352
   Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
paulson@17773
   353
   reapAll());
paulson@17488
   354
paulson@17772
   355
fun reapWatcher(pid, instr, outstr) = ignore
paulson@17484
   356
  (TextIO.closeIn instr; TextIO.closeOut outstr;
paulson@17772
   357
   Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
paulson@17772
   358
  handle OS.SysErr _ => ()
quigley@15642
   359
paulson@17772
   360
fun string_of_subgoal th i =
paulson@17772
   361
    string_of_cterm (List.nth(cprems_of th, i-1))
paulson@17772
   362
    handle Subscript => "Subgoal number out of range!"
paulson@17772
   363
paulson@17773
   364
fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
paulson@17773
   365
paulson@17772
   366
fun createWatcher (th, clause_arr) =
paulson@17773
   367
 let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (th,clause_arr)
paulson@17435
   368
     fun decr_watched() =
paulson@17502
   369
	  (goals_being_watched := !goals_being_watched - 1;
paulson@17435
   370
	   if !goals_being_watched = 0
paulson@17435
   371
	   then 
paulson@17716
   372
	     (debug ("\nReaping a watcher, childpid = "^
paulson@17773
   373
		     Int.toString (ResLib.intOfPid childpid));
paulson@17773
   374
	      killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
paulson@17435
   375
	    else ())
paulson@17772
   376
     val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of th);
paulson@17484
   377
     fun proofHandler n = 
paulson@17484
   378
       let val outcome = TextIO.inputLine childin
paulson@17772
   379
	   val probfile = TextIO.inputLine childin
paulson@17773
   380
	   val sgno = number_from_filename probfile
paulson@17773
   381
	   val text = string_of_subgoal th sgno
paulson@17484
   382
	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
paulson@17772
   383
		        "\"\nprobfile = " ^ probfile ^
paulson@17773
   384
		        "\nGoals being watched: "^  Int.toString (!goals_being_watched))
paulson@17502
   385
       in 
paulson@17502
   386
	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
paulson@17772
   387
	 then (priority (Recon_Transfer.apply_res_thm outcome);
paulson@17435
   388
	       decr_watched())
paulson@17484
   389
	 else if String.isPrefix "Invalid" outcome
paulson@17772
   390
	 then (priority ("Subgoal is not provable:\n" ^ text);
paulson@17484
   391
	       decr_watched())
paulson@17484
   392
	 else if String.isPrefix "Failure" outcome
paulson@17772
   393
	 then (priority ("Proof attempt failed:\n" ^ text);
paulson@17435
   394
	       decr_watched()) 
paulson@17216
   395
	(* print out a list of rules used from clasimpset*)
paulson@17484
   396
	 else if String.isPrefix "Success" outcome
paulson@17772
   397
	 then (priority (outcome ^ text);
paulson@17435
   398
	       decr_watched())
paulson@17216
   399
	  (* if proof translation failed *)
paulson@17484
   400
	 else if String.isPrefix "Translation failed" outcome
paulson@17772
   401
	 then (priority (outcome ^ text);
paulson@17435
   402
	       decr_watched())
paulson@17690
   403
	 else (priority "System error in proof handler";
paulson@17435
   404
	       decr_watched())
paulson@17484
   405
       end
paulson@17484
   406
 in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
paulson@17216
   407
    (childin, childout, childpid)
paulson@17216
   408
  end
quigley@15642
   409
quigley@15642
   410
end (* structure Watcher *)