src/HOL/Tools/ATP/watcher.ML
changeset 17764 fde495b9e24b
parent 17746 af59c748371d
child 17772 818cec5f82a4
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Wed Oct 05 10:56:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Oct 05 11:18:06 2005 +0200
     1.3 @@ -4,14 +4,11 @@
     1.4      Copyright   2004  University of Cambridge
     1.5   *)
     1.6  
     1.7 - (***************************************************************************)
     1.8 - (*  The watcher process starts a resolution process when it receives a     *)
     1.9 +(*  The watcher process starts a resolution process when it receives a     *)
    1.10  (*  message from Isabelle                                                  *)
    1.11  (*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    1.12  (*  and removes dead processes.  Also possible to kill all the resolution  *)
    1.13  (*  processes currently running.                                           *)
    1.14 -(*  Hardwired version of where to pick up the tptp files for the moment    *)
    1.15 -(***************************************************************************)
    1.16  
    1.17  signature WATCHER =
    1.18  sig
    1.19 @@ -23,17 +20,15 @@
    1.20      TextIO.outstream * (string*string*string*string*string) list 
    1.21      -> unit
    1.22  
    1.23 -(* Send message to watcher to kill currently running resolution provers *)
    1.24 +(* Send message to watcher to kill resolution provers *)
    1.25  val callSlayer : TextIO.outstream -> unit
    1.26  
    1.27  (* Start a watcher and set up signal handlers             *)
    1.28  val createWatcher : 
    1.29      thm * (ResClause.clause * thm) Array.array -> 
    1.30      TextIO.instream * TextIO.outstream * Posix.Process.pid
    1.31 -
    1.32 -(* Kill watcher process                                   *)
    1.33  val killWatcher : Posix.Process.pid -> unit
    1.34 -val killWatcher' : int -> unit
    1.35 +val setting_sep : char
    1.36  end
    1.37  
    1.38  
    1.39 @@ -41,6 +36,10 @@
    1.40  structure Watcher: WATCHER =
    1.41  struct
    1.42  
    1.43 +(*Field separators, used to pack items onto a text line*)
    1.44 +val command_sep = #"\t"
    1.45 +and setting_sep = #"%";
    1.46 +
    1.47  open Recon_Transfer
    1.48  
    1.49  val goals_being_watched = ref 0;
    1.50 @@ -134,8 +133,6 @@
    1.51  (*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
    1.52  (*****************************************************************************************)
    1.53  
    1.54 -    
    1.55 -(*Uses the $-character to separate items sent to watcher*)
    1.56  fun callResProvers (toWatcherStr,  []) = 
    1.57        (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
    1.58  |   callResProvers (toWatcherStr,
    1.59 @@ -144,9 +141,11 @@
    1.60        let val _ = trace (space_implode "\n" 
    1.61  		         (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
    1.62  			  probfile]))
    1.63 -      in TextIO.output (toWatcherStr,    
    1.64 -                        prover^"$"^proverCmd^"$"^ settings^"$"^probfile^"$\n");
    1.65 -         TextIO.output (toWatcherStr, String.toString goalstring^"\n");
    1.66 +      in TextIO.output (toWatcherStr,
    1.67 +                        (*Uses a special character to separate items sent to watcher*)
    1.68 +      	                space_implode (str command_sep)
    1.69 +                          [prover, proverCmd, settings, probfile,
    1.70 +                           String.toString goalstring ^ "\n"]);
    1.71                (*goalstring is a single string literal, with all specials escaped.*)
    1.72           goals_being_watched := (!goals_being_watched) + 1;
    1.73  	 TextIO.flushOut toWatcherStr;
    1.74 @@ -155,31 +154,29 @@
    1.75                                                  
    1.76                                      
    1.77   
    1.78 -(**************************************************************)
    1.79 -(* Send message to watcher to kill currently running vampires *)
    1.80 -(**************************************************************)
    1.81  
    1.82 -fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n"); 
    1.83 +(*Send message to watcher to kill currently running vampires. NOT USED and possibly
    1.84 +  buggy. Note that killWatcher kills the entire process group anyway.*)
    1.85 +fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n"); 
    1.86                              TextIO.flushOut toWatcherStr)
    1.87  
    1.88                      
    1.89  (**************************************************************)
    1.90  (* Get commands from Isabelle                                 *)
    1.91  (**************************************************************)
    1.92 -fun getCmds (toParentStr,fromParentStr, cmdList) = 
    1.93 +fun getCmds (toParentStr, fromParentStr, cmdList) = 
    1.94    let val thisLine = TextIO.inputLine fromParentStr 
    1.95 -      val _ = trace("\nGot command from parent: " ^ thisLine)
    1.96    in
    1.97 +     trace("\nGot command from parent: " ^ thisLine);
    1.98       if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
    1.99       else if thisLine = "Kill children\n"
   1.100 -     then (TextIO.output (toParentStr,thisLine ); 
   1.101 +     then (TextIO.output (toParentStr,thisLine); 
   1.102  	   TextIO.flushOut toParentStr;
   1.103 -	   (("","","Kill children",[],"")::cmdList)  )
   1.104 +	   [("","","Kill children",[],"")])
   1.105       else
   1.106 -       let val [prover,proverCmd,settingstr,probfile,_] = 
   1.107 -                   String.tokens (fn c => c = #"$") thisLine
   1.108 -           val settings = String.tokens (fn c => c = #"%") settingstr
   1.109 -	   val goalstring = TextIO.inputLine fromParentStr 
   1.110 +       let val [prover,proverCmd,settingstr,probfile,goalstring] = 
   1.111 +                   String.tokens (fn c => c = command_sep) thisLine
   1.112 +           val settings = String.tokens (fn c => c = setting_sep) settingstr
   1.113         in
   1.114             trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd^
   1.115                    "  problem file: " ^ probfile ^ 
   1.116 @@ -187,6 +184,9 @@
   1.117             getCmds (toParentStr, fromParentStr, 
   1.118                      (prover, goalstring, proverCmd, settings, probfile)::cmdList) 
   1.119         end
   1.120 +       handle Bind => 
   1.121 +          (trace "getCmds: command parsing failed!";
   1.122 +           getCmds (toParentStr, fromParentStr, cmdList))
   1.123    end
   1.124  	    
   1.125                                                                    
   1.126 @@ -212,8 +212,6 @@
   1.127  (*  Set up a Watcher Process         *)
   1.128  (*************************************)
   1.129  
   1.130 -fun getProofCmd (a,c,d,e,f) = d
   1.131 -
   1.132  (* for tracing: encloses each string element in brackets. *)
   1.133  val concat_with_and = space_implode " & " o map (enclose "(" ")");
   1.134  
   1.135 @@ -246,40 +244,34 @@
   1.136  
   1.137  fun setupWatcher (thm,clause_arr) = 
   1.138    let
   1.139 -    (** pipes for communication between parent and watcher **)
   1.140 -    val p1 = Posix.IO.pipe ()
   1.141 +    val p1 = Posix.IO.pipe ()   (** pipes for communication between parent and watcher **)
   1.142      val p2 = Posix.IO.pipe ()
   1.143      fun closep () = 
   1.144 -	 (Posix.IO.close (#outfd p1); 
   1.145 -	  Posix.IO.close (#infd p1);
   1.146 -	  Posix.IO.close (#outfd p2); 
   1.147 -	  Posix.IO.close (#infd p2))
   1.148 -    (***********************************************************)
   1.149 -    (****** fork a watcher process and get it set up and going *)
   1.150 -    (***********************************************************)
   1.151 +	 (Posix.IO.close (#outfd p1); Posix.IO.close (#infd p1);
   1.152 +	  Posix.IO.close (#outfd p2); Posix.IO.close (#infd p2))
   1.153 +    (****** fork a watcher process and get it set up and going ******)
   1.154      fun startWatcher procList =
   1.155 -     (case  Posix.Process.fork() (***************************************)
   1.156 -      of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   1.157 -				    (***************************************)
   1.158 -
   1.159 -				      (*************************)
   1.160 -       | NONE => let                  (* child - i.e. watcher  *)
   1.161 -	  val oldchildin = #infd p1   (*************************)
   1.162 +     (case  Posix.Process.fork() 
   1.163 +      of SOME pid => pid (* parent - i.e. main Isabelle process *)
   1.164 +       | NONE => let                (* child - i.e. watcher  *)
   1.165 +	  val oldchildin = #infd p1  
   1.166  	  val fromParent = Posix.FileSys.wordToFD 0w0
   1.167  	  val oldchildout = #outfd p2
   1.168  	  val toParent = Posix.FileSys.wordToFD 0w1
   1.169  	  val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   1.170  	  val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   1.171  	  val toParentStr = openOutFD ("_exec_out_parent", toParent)
   1.172 -	  val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   1.173 +	  val pid = Posix.ProcEnv.getpid()
   1.174 +	  val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
   1.175 +                   (*set process group id: allows killing all children*)
   1.176 +	  val () = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   1.177  	 
   1.178  	  fun pollChildInput fromStr = 
   1.179  	     case getInIoDesc fromStr of
   1.180  	       SOME iod => 
   1.181  		 (case OS.IO.pollDesc iod of
   1.182  		    SOME pd =>
   1.183 -			let val pd' = OS.IO.pollIn pd
   1.184 -			in
   1.185 +			let val pd' = OS.IO.pollIn pd in
   1.186  			  case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
   1.187  			      [] => false
   1.188  			    | pd''::_ => OS.IO.isIn pd''
   1.189 @@ -287,7 +279,6 @@
   1.190  		   | NONE => false)
   1.191  	     | NONE => false
   1.192  
   1.193 -
   1.194  	  (* Check all ATP processes currently running for output                 *)
   1.195  	  fun checkChildren ([], toParentStr) = []  (* no children to check *)
   1.196  	  |   checkChildren (childProc::otherChildren, toParentStr) = 
   1.197 @@ -295,8 +286,7 @@
   1.198  			          Int.toString (length (childProc::otherChildren)))
   1.199  		   val (childInput,childOutput) = cmdstreamsOf childProc
   1.200  		   val child_handle = cmdchildHandle childProc
   1.201 -		   (* childCmd is the file that the problem is in *)
   1.202 -		   val childCmd = fst(snd (cmdchildInfo childProc))
   1.203 +		   val childCmd = #1(#2(cmdchildInfo childProc)) (*name of problem file*)
   1.204  		   val _ = trace ("\nchildCmd = " ^ childCmd)
   1.205  		   val sg_num = number_from_filename childCmd
   1.206  		   val childIncoming = pollChildInput childInput
   1.207 @@ -307,10 +297,8 @@
   1.208  	       in 
   1.209  		 trace("\nsubgoals forked to checkChildren: " ^ goalstring);
   1.210  		 if childIncoming
   1.211 -		 then 
   1.212 -		   (* check here for prover label on child*)
   1.213 -		   let val _ = trace ("\nInput available from child: " ^
   1.214 -				      childCmd ^ 
   1.215 +		 then (* check here for prover label on child*)
   1.216 +		   let val _ = trace ("\nInput available from child: " ^ childCmd ^ 
   1.217  				      "\ngoalstring is " ^ goalstring)
   1.218  		       val childDone = (case prover of
   1.219  			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
   1.220 @@ -331,138 +319,90 @@
   1.221  	       end
   1.222  
   1.223  	
   1.224 -     (********************************************************************)                  
   1.225 -     (* call resolution processes                                        *)
   1.226 -     (* settings should be a list of strings                             *)
   1.227 -     (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
   1.228 -     (* takes list of (string, string, string list, string)list proclist *)
   1.229 -     (********************************************************************)
   1.230 -
   1.231 -
   1.232 -(*** add subgoal id num to this *)
   1.233 -	fun execCmds  [] procList = procList
   1.234 -	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   1.235 -	      let val _ = trace 
   1.236 -	                    (space_implode "\n" 
   1.237 -	                      (["\nAbout to execute command for goal:",
   1.238 -	                        goalstring, proverCmd] @ settings @
   1.239 -	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   1.240 +	(* call resolution processes                                        *)
   1.241 +	(* settings should be a list of strings  ["-t 300", "-m 100000"]    *)
   1.242 +	(* takes list of (string, string, string list, string)list proclist *)
   1.243 +	fun execCmds [] procList = procList
   1.244 +	|   execCmds ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   1.245 +	      let val _ = trace (space_implode "\n" 
   1.246 +				 (["\nAbout to execute command for goal:",
   1.247 +				   goalstring, proverCmd] @ settings @
   1.248 +				  [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   1.249  	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   1.250 -		       (Unix.execute(proverCmd, (settings@[file])))
   1.251 +		       Unix.execute(proverCmd, settings@[file])
   1.252  		  val (instr, outstr) = Unix.streamsOf childhandle
   1.253 -		  val newProcList = (CMDPROC{
   1.254 -				       prover = prover,
   1.255 -				       cmd = file,
   1.256 -				       goalstring = goalstring,
   1.257 -				       proc_handle = childhandle,
   1.258 -				       instr = instr,
   1.259 -				       outstr = outstr }) :: procList
   1.260 +		  val newProcList = CMDPROC{prover = prover,
   1.261 +					    cmd = file,
   1.262 +					    goalstring = goalstring,
   1.263 +					    proc_handle = childhandle,
   1.264 +					    instr = instr,
   1.265 +					    outstr = outstr} :: procList
   1.266       
   1.267  		  val _ = trace ("\nFinished at " ^
   1.268  			         Date.toString(Date.fromTimeLocal(Time.now())))
   1.269  	      in execCmds cmds newProcList end
   1.270  
   1.271 -
   1.272 -     (****************************************)                  
   1.273 -     (* call resolution processes remotely   *)
   1.274 -     (* settings should be a list of strings *)
   1.275 -     (* e.g. ["-t300", "-m100000"]         *)
   1.276 -     (****************************************)
   1.277 -
   1.278 -      (*  fun execRemoteCmds  [] procList = procList
   1.279 -	|   execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList  =  
   1.280 -	      let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   1.281 -		  in
   1.282 -		       execRemoteCmds  cmds newProcList
   1.283 -		  end
   1.284 -*)
   1.285 -
   1.286 -     (**********************************************)                  
   1.287 -     (* Watcher Loop                               *)
   1.288 -     (**********************************************)
   1.289 -         val iterations_left = ref 500;  (*don't let it run forever*)
   1.290 +         (******** Watcher Loop ********)
   1.291 +         val limit = ref 500;  (*don't let it run forever*)
   1.292  
   1.293  	 fun keepWatching (procList) = 
   1.294  	   let fun loop procList =  
   1.295 -		let val _ = trace ("\nCalling pollParentInput: " ^ 
   1.296 -			           Int.toString (!iterations_left));
   1.297 -		    val cmdsFromIsa = pollParentInput 
   1.298 -		                       (fromParentIOD, fromParentStr, toParentStr)
   1.299 -		in 
   1.300 -		   OS.Process.sleep (Time.fromMilliseconds 100);
   1.301 -		   iterations_left := !iterations_left - 1;
   1.302 -		   if !iterations_left <= 0 
   1.303 -		   then 
   1.304 -		    (trace "\nTimeout: Killing proof processes";
   1.305 -	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   1.306 -		     TextIO.flushOut toParentStr;
   1.307 -		     killChildren (map cmdchildHandle procList);
   1.308 -		     exit 0)
   1.309 -		   else if isSome cmdsFromIsa
   1.310 -		   then (*  deal with input from Isabelle *)
   1.311 -		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
   1.312 -		     then 
   1.313 +	      let val _ = trace ("\nCalling pollParentInput: " ^ Int.toString (!limit));
   1.314 +		  val cmdsFromIsa = pollParentInput 
   1.315 +				     (fromParentIOD, fromParentStr, toParentStr)
   1.316 +	      in 
   1.317 +		 OS.Process.sleep (Time.fromMilliseconds 100);
   1.318 +		 limit := !limit - 1;
   1.319 +		 if !limit = 0 
   1.320 +		 then 
   1.321 +		  (trace "\nTimeout: Killing proof processes";
   1.322 +		   TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   1.323 +		   TextIO.flushOut toParentStr;
   1.324 +		   killChildren (map cmdchildHandle procList);
   1.325 +		   exit 0)
   1.326 +		 else case cmdsFromIsa of
   1.327 +		     SOME [(_,_,"Kill children",_,_)] => 
   1.328  		       let val child_handles = map cmdchildHandle procList 
   1.329 -		       in
   1.330 -			  killChildren child_handles;
   1.331 -			  loop []
   1.332 -		       end
   1.333 -		     else
   1.334 -		       if length procList < 5     (********************)
   1.335 +		       in  killChildren child_handles; loop []  end
   1.336 +		   | SOME cmds => (*  deal with commands from Isabelle process *)
   1.337 +		       if length procList < 40
   1.338  		       then                        (* Execute locally  *)
   1.339  			 let 
   1.340 -			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.341 -			   val _ = Posix.ProcEnv.getppid()
   1.342 -			   val _ = trace "\nJust execed a child"
   1.343 +			   val newProcList = execCmds cmds procList
   1.344  			   val newProcList' = checkChildren (newProcList, toParentStr) 
   1.345  			 in
   1.346 -			   trace ("\nOff to keep watching: " ^ 
   1.347 -			          Int.toString (!iterations_left));
   1.348 -			   loop newProcList'
   1.349 +			   trace "\nJust execed a child"; loop newProcList'
   1.350  			 end
   1.351 -		       else  (* Execute remotely              *)
   1.352 -			     (* (actually not remote for now )*)
   1.353 +		       else  (* Execute remotely [FIXME: NOT REALLY]  *)
   1.354  			 let 
   1.355 -			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.356 -			   val _ = Posix.ProcEnv.getppid()
   1.357 -			   val newProcList' =checkChildren (newProcList, toParentStr) 
   1.358 -			 in
   1.359 -			   loop newProcList'
   1.360 -			 end
   1.361 -		   else (* No new input from Isabelle *)
   1.362 -		     let val newProcList = checkChildren (procList, toParentStr)
   1.363 -		     in
   1.364 -		       trace ("\nNo new input, still watching: " ^ 
   1.365 -			      Int.toString (!iterations_left));
   1.366 -		       loop newProcList
   1.367 -		     end
   1.368 -		 end
   1.369 +			   val newProcList = execCmds cmds procList
   1.370 +			   val newProcList' = checkChildren (newProcList, toParentStr) 
   1.371 +			 in loop newProcList' end
   1.372 +		   | NONE => (* No new input from Isabelle *)
   1.373 +		       let val newProcList = checkChildren (procList, toParentStr)
   1.374 +		       in
   1.375 +			 trace "\nNo new input, still watching"; loop newProcList
   1.376 +		       end
   1.377 +	       end
   1.378  	   in  
   1.379  	       loop procList
   1.380  	   end
   1.381  	   
   1.382  
   1.383 -	   in
   1.384 -	    (***************************)
   1.385 -	    (*** Sort out pipes ********)
   1.386 -	    (***************************)
   1.387 +	 in
   1.388 +	  (*** Sort out pipes ********)
   1.389 +	   Posix.IO.close (#outfd p1);
   1.390 +	   Posix.IO.close (#infd p2);
   1.391 +	   Posix.IO.dup2{old = oldchildin, new = fromParent};
   1.392 +	   Posix.IO.close oldchildin;
   1.393 +	   Posix.IO.dup2{old = oldchildout, new = toParent};
   1.394 +	   Posix.IO.close oldchildout;
   1.395  
   1.396 -	     Posix.IO.close (#outfd p1);
   1.397 -	     Posix.IO.close (#infd p2);
   1.398 -	     Posix.IO.dup2{old = oldchildin, new = fromParent};
   1.399 -	     Posix.IO.close oldchildin;
   1.400 -	     Posix.IO.dup2{old = oldchildout, new = toParent};
   1.401 -	     Posix.IO.close oldchildout;
   1.402 -
   1.403 -	     (***************************)
   1.404 -	     (* start the watcher loop  *)
   1.405 -	     (***************************)
   1.406 -	     keepWatching (procList);
   1.407 -	     (****************************************************************************)
   1.408 -(* fake return value - actually want the watcher to loop until killed *)
   1.409 -	     (****************************************************************************)
   1.410 -	     Posix.Process.wordToPid 0w0
   1.411 -	   end);
   1.412 +	   (* start the watcher loop  *)
   1.413 +	   keepWatching (procList);
   1.414 +	   (* fake return value - actually want the watcher to loop until killed *)
   1.415 +	   Posix.Process.wordToPid 0w0
   1.416 +	 end);
   1.417       (* end case *)
   1.418  
   1.419  
   1.420 @@ -503,9 +443,7 @@
   1.421  (* Start a watcher and set up signal handlers             *)
   1.422  (**********************************************************)
   1.423  
   1.424 -fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   1.425 -
   1.426 -val killWatcher' = killWatcher o ResLib.pidOfInt;
   1.427 +fun killWatcher pid = Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
   1.428  
   1.429  fun reapWatcher(pid, instr, outstr) =
   1.430    (TextIO.closeIn instr; TextIO.closeOut outstr;