src/HOL/Tools/ATP/watcher.ML
changeset 17568 e93f7510e1e1
parent 17525 ae5bb6001afb
child 17583 c272b91b619f
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Wed Sep 21 18:06:04 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Sep 21 18:35:19 2005 +0200
     1.3 @@ -16,36 +16,24 @@
     1.4  signature WATCHER =
     1.5  sig
     1.6  
     1.7 -(*****************************************************************************************)
     1.8  (*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
     1.9 -(*  callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list             *)
    1.10 -(*****************************************************************************************)
    1.11 +(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
    1.12  
    1.13  val callResProvers :
    1.14      TextIO.outstream * (string*string*string*string*string) list 
    1.15      -> unit
    1.16  
    1.17 -(************************************************************************)
    1.18  (* Send message to watcher to kill currently running resolution provers *)
    1.19 -(************************************************************************)
    1.20 -
    1.21  val callSlayer : TextIO.outstream -> unit
    1.22  
    1.23 -(**********************************************************)
    1.24  (* Start a watcher and set up signal handlers             *)
    1.25 -(**********************************************************)
    1.26 -
    1.27  val createWatcher : 
    1.28      thm * (ResClause.clause * thm) Array.array -> 
    1.29      TextIO.instream * TextIO.outstream * Posix.Process.pid
    1.30  
    1.31 -(**********************************************************)
    1.32  (* Kill watcher process                                   *)
    1.33 -(**********************************************************)
    1.34 -
    1.35  val killWatcher : Posix.Process.pid -> unit
    1.36  val killWatcher' : int -> unit
    1.37 -
    1.38  end
    1.39  
    1.40  
    1.41 @@ -57,42 +45,32 @@
    1.42  
    1.43  val goals_being_watched = ref 0;
    1.44  
    1.45 -(*****************************************)
    1.46  (*  The result of calling createWatcher  *)
    1.47 -(*****************************************)
    1.48 -
    1.49  datatype proc = PROC of {
    1.50          pid : Posix.Process.pid,
    1.51          instr : TextIO.instream,
    1.52          outstr : TextIO.outstream
    1.53        };
    1.54  
    1.55 -(*****************************************)
    1.56  (*  The result of calling executeToList  *)
    1.57 -(*****************************************)
    1.58 -
    1.59  datatype cmdproc = CMDPROC of {
    1.60 -        prover: string,             (* Name of the resolution prover used, e.g. Vampire, SPASS *)
    1.61 -        cmd:  string,              (* The file containing the goal for res prover to prove *)     
    1.62 -        goalstring: string,         (* string representation of subgoal*) 
    1.63 +        prover: string,       (* Name of the resolution prover used, e.g. Vampire*)
    1.64 +        cmd:  string,         (* The file containing the goal for res prover to prove *)     
    1.65 +        goalstring: string,   (* string representation of subgoal*) 
    1.66          proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    1.67          instr : TextIO.instream,   (*  Input stream to child process *)
    1.68 -        outstr : TextIO.outstream  (*  Output stream from child process *)
    1.69 -      };
    1.70 +        outstr : TextIO.outstream};  (*  Output stream from child process *)
    1.71  
    1.72  type signal = Posix.Signal.signal
    1.73  datatype exit_status = datatype Posix.Process.exit_status
    1.74  
    1.75  val fromStatus = Posix.Process.fromStatus
    1.76  
    1.77 -
    1.78  fun reap(pid, instr, outstr) =
    1.79    let val u = TextIO.closeIn instr;
    1.80        val u = TextIO.closeOut outstr;
    1.81        val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    1.82 -  in
    1.83 -	  status
    1.84 -  end
    1.85 +  in status end
    1.86  
    1.87  fun fdReader (name : string, fd : Posix.IO.file_desc) =
    1.88  	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    1.89 @@ -134,19 +112,14 @@
    1.90    goalstring;
    1.91  
    1.92  
    1.93 -(********************************************************************************)
    1.94  (*    gets individual args from instream and concatenates them into a list      *)
    1.95 -(********************************************************************************)
    1.96 -
    1.97  fun getArgs (fromParentStr, toParentStr, ys) =  
    1.98    let val thisLine = TextIO.input fromParentStr
    1.99    in ys@[thisLine] end
   1.100  
   1.101                              
   1.102 -(********************************************************************************)
   1.103  (*  Send request to Watcher for a vampire to be called for filename in arg      *)
   1.104 -(********************************************************************************)
   1.105 -                    
   1.106 +                   
   1.107  fun callResProver (toWatcherStr,  arg) = 
   1.108        (TextIO.output (toWatcherStr, arg^"\n"); 
   1.109         TextIO.flushOut toWatcherStr)
   1.110 @@ -223,21 +196,17 @@
   1.111    let val thisLine = TextIO.inputLine fromParentStr 
   1.112        val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
   1.113    in
   1.114 -     if thisLine = "End of calls\n" then cmdList
   1.115 +     if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
   1.116       else if thisLine = "Kill children\n"
   1.117 -     then 
   1.118 -	 (   TextIO.output (toParentStr,thisLine ); 
   1.119 -	     TextIO.flushOut toParentStr;
   1.120 -	   (("","","Kill children",[],"")::cmdList)
   1.121 -	  )
   1.122 +     then (TextIO.output (toParentStr,thisLine ); 
   1.123 +	   TextIO.flushOut toParentStr;
   1.124 +	   (("","","Kill children",[],"")::cmdList)  )
   1.125       else let val thisCmd = getCmd thisLine 
   1.126  	       (*********************************************************)
   1.127  	       (* thisCmd = (prover,proverCmd, settings, file)*)
   1.128  	       (* i.e. put back into tuple format                       *)
   1.129  	       (*********************************************************)
   1.130  	   in
   1.131 -	     (*TextIO.output (toParentStr, thisCmd); 
   1.132 -	       TextIO.flushOut toParentStr;*)
   1.133  	       getCmds (toParentStr, fromParentStr, thisCmd::cmdList)
   1.134  	   end
   1.135    end
   1.136 @@ -274,6 +243,24 @@
   1.137  
   1.138  fun killChildren procs = List.app (ignore o killChild) procs;
   1.139  
   1.140 + (*************************************************************)
   1.141 + (* take an instream and poll its underlying reader for input *)
   1.142 + (*************************************************************)
   1.143 + 
   1.144 + fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = 
   1.145 +   case OS.IO.pollDesc fromParentIOD
   1.146 +   of SOME pd =>
   1.147 +       let val pd' = OS.IO.pollIn pd
   1.148 +	   val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   1.149 +       in
   1.150 +	  if null pdl 
   1.151 +	  then NONE
   1.152 +	  else if OS.IO.isIn (hd pdl)
   1.153 +	       then SOME (getCmds (toParentStr, fromParentStr, []))
   1.154 +	       else NONE
   1.155 +       end
   1.156 +   | NONE => NONE;
   1.157 +
   1.158  fun setupWatcher (thm,clause_arr) = 
   1.159    let
   1.160      (** pipes for communication between parent and watcher **)
   1.161 @@ -302,30 +289,7 @@
   1.162  	   val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   1.163  	   val toParentStr = openOutFD ("_exec_out_parent", toParent)
   1.164  	   val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   1.165 -
   1.166 -	 (*************************************************************)
   1.167 -	 (* take an instream and poll its underlying reader for input *)
   1.168 -	 (*************************************************************)
   1.169 -
   1.170 -	 fun pollParentInput () = 
   1.171 -	   let val pd = OS.IO.pollDesc fromParentIOD
   1.172 -	   in 
   1.173 -	     if isSome pd then 
   1.174 -		 let val pd' = OS.IO.pollIn (valOf pd)
   1.175 -		     val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   1.176 -		     val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
   1.177 -		       ("In parent_poll\n")	
   1.178 -		 in
   1.179 -		    if null pdl 
   1.180 -		    then
   1.181 -		       NONE
   1.182 -		    else if (OS.IO.isIn (hd pdl)) 
   1.183 -			 then SOME (getCmds (toParentStr, fromParentStr, []))
   1.184 -			 else NONE
   1.185 -		 end
   1.186 -	       else NONE
   1.187 -	   end
   1.188 -		 
   1.189 +	 
   1.190  	  fun pollChildInput fromStr = 
   1.191  	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
   1.192  			 ("In child_poll\n")
   1.193 @@ -345,7 +309,7 @@
   1.194  			 NONE)
   1.195  		      else if OS.IO.isIn (hd pdl)
   1.196  		      then
   1.197 -			   let val inval =  (TextIO.inputLine fromStr)
   1.198 +			   let val inval = TextIO.inputLine fromStr
   1.199  			       val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
   1.200  			   in SOME inval end
   1.201  		      else
   1.202 @@ -355,21 +319,23 @@
   1.203  		 else NONE
   1.204  		 end
   1.205  	     else NONE
   1.206 -	end
   1.207 -
   1.208 +	   end
   1.209  
   1.210 -	(****************************************************************************)
   1.211 -	(* Check all vampire processes currently running for output                 *)
   1.212 -	(****************************************************************************) 
   1.213 +         val cc_iterations_left = ref 50;  
   1.214 +         (*FIXME: why does this loop if not explicitly bounded?*)
   1.215 +
   1.216 +	(* Check all ATP processes currently running for output                 *)
   1.217  						   (*********************************)
   1.218  	 fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   1.219  						   (*********************************)
   1.220  	 |   checkChildren ((childProc::otherChildren), toParentStr) = 
   1.221  	       let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
   1.222  			      ("In check child, length of queue:"^
   1.223 -			       string_of_int (length (childProc::otherChildren)))
   1.224 -		   val (childInput,childOutput) =  cmdstreamsOf childProc
   1.225 -		   val child_handle= cmdchildHandle childProc
   1.226 +			        Int.toString (length (childProc::otherChildren)) ^
   1.227 +			       "\niterations left = " ^ Int.toString (!cc_iterations_left))
   1.228 +		   val _ = Posix.Process.sleep (Time.fromMilliseconds 50) (*slow the looping*)
   1.229 +		   val (childInput,childOutput) = cmdstreamsOf childProc
   1.230 +		   val child_handle = cmdchildHandle childProc
   1.231  		   (* childCmd is the .dfg file that the problem is in *)
   1.232  		   val childCmd = fst(snd (cmdchildInfo childProc))
   1.233  		   val _ = File.append (File.tmp_path (Path.basic "child_check")) 
   1.234 @@ -395,11 +361,16 @@
   1.235  		             ("\nsubgoals forked to checkChildren: " ^ 
   1.236  		              space_implode "\n" [prems_string,prover,goalstring])
   1.237  	       in 
   1.238 -		 if isSome childIncoming
   1.239 +	         cc_iterations_left := !cc_iterations_left - 1;
   1.240 +		 if !cc_iterations_left = 0 then [] (*Abandon looping!*)
   1.241 +		 else if isSome childIncoming
   1.242  		 then 
   1.243  		   (* check here for prover label on child*)
   1.244  		   let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
   1.245 -			         "\nInput available from childIncoming" 
   1.246 +			        ("\nInput available from childIncoming" ^
   1.247 +			         "\nchecking if proof found." ^
   1.248 +			         "\nchildCmd is " ^ childCmd ^ 
   1.249 +			         "\ngoalstring is: " ^ goalstring ^ "\n\n")
   1.250  		       val childDone = (case prover of
   1.251  			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
   1.252  			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
   1.253 @@ -478,17 +449,23 @@
   1.254       (**********************************************)                  
   1.255       (* Watcher Loop                               *)
   1.256       (**********************************************)
   1.257 -         val iterations_left = ref 1000;  (*200 seconds, 5 iterations per sec*)
   1.258 +         val iterations_left = ref 100;  (*don't let it run forever*)
   1.259  
   1.260 -	 fun keepWatching (toParentStr, fromParentStr,procList) = 
   1.261 +	 fun keepWatching (procList) = 
   1.262  	   let fun loop procList =  
   1.263  		let val _ = Posix.Process.sleep (Time.fromMilliseconds 200)
   1.264 -		    val cmdsFromIsa = pollParentInput ()
   1.265 +		    val _ = File.append (File.tmp_path (Path.basic "keep_watch")) 
   1.266 +			       ("\nCalling pollParentInput: " ^ 
   1.267 +			        Int.toString (!iterations_left));
   1.268 +		    val cmdsFromIsa = pollParentInput 
   1.269 +		                       (fromParentIOD, fromParentStr, toParentStr)
   1.270  		in 
   1.271  		   iterations_left := !iterations_left - 1;
   1.272 -		   if !iterations_left = 0 
   1.273 +		   if !iterations_left <= 0 
   1.274  		   then (*Sadly, this code fails to terminate the watcher!*)
   1.275 -		    (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   1.276 +		    (File.append (File.tmp_path (Path.basic "keep_watch")) 
   1.277 +			         "\nTimeout: Killing proof processes";
   1.278 +	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   1.279  		     TextIO.flushOut toParentStr;
   1.280  		     killChildren (map cmdchildHandle procList))
   1.281  		   else if isSome cmdsFromIsa
   1.282 @@ -505,20 +482,21 @@
   1.283  		       then                        (* Execute locally  *)
   1.284  			 let 
   1.285  			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.286 -			   val parentID = Posix.ProcEnv.getppid()
   1.287 -			      val _ = File.append (File.tmp_path (Path.basic "prekeep_watch"))
   1.288 -			      "Just execed a child\n"
   1.289 +			   val _ = Posix.ProcEnv.getppid()
   1.290 +			   val _ = File.append (File.tmp_path (Path.basic "keep_watch"))
   1.291 +			      "\nJust execed a child"
   1.292  			   val newProcList' = checkChildren (newProcList, toParentStr) 
   1.293  			 in
   1.294  			   File.append (File.tmp_path (Path.basic "keep_watch")) 
   1.295 -			       "Off to keep watching...\n";
   1.296 +			       ("\nOff to keep watching: " ^ 
   1.297 +			        Int.toString (!iterations_left));
   1.298  			   loop newProcList'
   1.299  			 end
   1.300  		       else  (* Execute remotely              *)
   1.301  			     (* (actually not remote for now )*)
   1.302  			 let 
   1.303  			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.304 -			   val parentID = Posix.ProcEnv.getppid()
   1.305 +			   val _ = Posix.ProcEnv.getppid()
   1.306  			   val newProcList' =checkChildren (newProcList, toParentStr) 
   1.307  			 in
   1.308  			   loop newProcList'
   1.309 @@ -526,7 +504,9 @@
   1.310  		   else (* No new input from Isabelle *)
   1.311  		     let val newProcList = checkChildren (procList, toParentStr)
   1.312  		     in
   1.313 -		      (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...2\n ");
   1.314 +		       File.append (File.tmp_path (Path.basic "keep_watch")) 
   1.315 +			       ("\nNo new input, still watching: " ^ 
   1.316 +			        Int.toString (!iterations_left));
   1.317  		       loop newProcList
   1.318  		     end
   1.319  		 end
   1.320 @@ -550,7 +530,7 @@
   1.321  	     (***************************)
   1.322  	     (* start the watcher loop  *)
   1.323  	     (***************************)
   1.324 -	     keepWatching (toParentStr, fromParentStr, procList);
   1.325 +	     keepWatching (procList);
   1.326  	     (****************************************************************************)
   1.327  (* fake return value - actually want the watcher to loop until killed *)
   1.328  	     (****************************************************************************)
   1.329 @@ -574,24 +554,21 @@
   1.330      val instr = openInFD ("_exec_in", #infd p2)
   1.331      val outstr = openOutFD ("_exec_out", #outfd p1)
   1.332      
   1.333 -    in
   1.334 -     (*******************************)
   1.335 -     (* close the child-side fds    *)
   1.336 -     (*******************************)
   1.337 -      Posix.IO.close (#outfd p2);
   1.338 -      Posix.IO.close (#infd p1);
   1.339 -      (* set the fds close on exec *)
   1.340 -      Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   1.341 -      Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   1.342 -       
   1.343 -     (*******************************)
   1.344 -     (* return value                *)
   1.345 -     (*******************************)
   1.346 -      PROC{pid = pid,
   1.347 -	instr = instr,
   1.348 -	outstr = outstr
   1.349 -      }
   1.350 -   end;
   1.351 +  in
   1.352 +   (*******************************)
   1.353 +   (* close the child-side fds    *)
   1.354 +   (*******************************)
   1.355 +    Posix.IO.close (#outfd p2);
   1.356 +    Posix.IO.close (#infd p1);
   1.357 +    (* set the fds close on exec *)
   1.358 +    Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   1.359 +    Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   1.360 +     
   1.361 +   (*******************************)
   1.362 +   (* return value                *)
   1.363 +   (*******************************)
   1.364 +    PROC{pid = pid, instr = instr, outstr = outstr}
   1.365 +  end;
   1.366  
   1.367  
   1.368  
   1.369 @@ -624,7 +601,7 @@
   1.370  	   val goalstring = TextIO.inputLine childin
   1.371  	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
   1.372  		        "\"\ngoalstring = " ^ goalstring ^
   1.373 -		        "\ngoals_being_watched: "^ string_of_int (!goals_being_watched))
   1.374 +		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
   1.375         in 
   1.376  	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
   1.377  	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));