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