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