src/HOL/Tools/ATP/watcher.ML
changeset 17690 8ba7c3cd24a8
parent 17583 c272b91b619f
child 17716 89932e53f31d
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Wed Sep 28 11:15:33 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Sep 28 11:16:27 2005 +0200
     1.3 @@ -47,6 +47,8 @@
     1.4  
     1.5  val trace_path = Path.basic "watcher_trace";
     1.6  
     1.7 +fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
     1.8 +              else ();
     1.9  
    1.10  (*  The result of calling createWatcher  *)
    1.11  datatype proc = PROC of {
    1.12 @@ -139,9 +141,9 @@
    1.13  |   callResProvers (toWatcherStr,
    1.14                      (prover,goalstring, proverCmd,settings, 
    1.15                       probfile)  ::  args) =
    1.16 -      let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
    1.17 -                             (prover^goalstring^proverCmd^settings^
    1.18 -                              probfile)
    1.19 +      let val _ = trace (space_implode "\n" 
    1.20 +		         (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
    1.21 +			  probfile]))
    1.22        in TextIO.output (toWatcherStr,    
    1.23              (prover^"$"^goalstring^"$"^proverCmd^"$"^
    1.24               settings^"$"^probfile^"\n"));
    1.25 @@ -160,44 +162,29 @@
    1.26                              TextIO.flushOut toWatcherStr)
    1.27  
    1.28  
    1.29 -
    1.30  (**************************************************************)
    1.31  (* Remove \n token from a vampire goal filename and extract   *)
    1.32  (* prover, proverCmd, settings and file from input string     *)
    1.33  (**************************************************************)
    1.34  
    1.35 -fun separateFields str =
    1.36 -  let val _ = File.append (File.tmp_path (Path.basic "sep_field"))
    1.37 -                          ("In separateFields, str is: " ^ str ^ "\n\n") 
    1.38 -      val [prover,goalstring,proverCmd,settingstr,probfile] = 
    1.39 -          String.tokens (fn c => c = #"$") str
    1.40 -      val settings = String.tokens (fn c => c = #"%") settingstr
    1.41 -      val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
    1.42 -                  ("Sep comms are: "^ str ^"**"^
    1.43 -                   prover^" goalstr:  "^goalstring^
    1.44 -                   "\n provercmd: "^proverCmd^
    1.45 -                   "\n prob  "^probfile^"\n\n")
    1.46 -  in
    1.47 -     (prover,goalstring, proverCmd, settings, probfile)
    1.48 -  end
    1.49 -
    1.50  val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
    1.51  
    1.52  fun getCmd cmdStr = 
    1.53 -  let val cmdStr' = remove_newlines cmdStr
    1.54 -  in
    1.55 -      File.write (File.tmp_path (Path.basic"sepfields_call")) 
    1.56 -		 ("about to call separateFields with " ^ cmdStr');
    1.57 -      separateFields cmdStr'
    1.58 -  end;
    1.59 +  let val [prover,goalstring,proverCmd,settingstr,probfile] = 
    1.60 +            String.tokens (fn c => c = #"$") (remove_newlines cmdStr)
    1.61 +      val settings = String.tokens (fn c => c = #"%") settingstr
    1.62 +      val _ = trace ("getCmd: " ^ cmdStr ^
    1.63 +		    "\nprover" ^ prover ^ " goalstr:  "^goalstring^
    1.64 +		    "\nprovercmd: " ^ proverCmd^
    1.65 +		    "\nprob  " ^ probfile ^ "\n\n")
    1.66 +  in (prover,goalstring, proverCmd, settings, probfile) end
    1.67                        
    1.68  (**************************************************************)
    1.69  (* Get commands from Isabelle                                 *)
    1.70  (**************************************************************)
    1.71 -
    1.72  fun getCmds (toParentStr,fromParentStr, cmdList) = 
    1.73    let val thisLine = TextIO.inputLine fromParentStr 
    1.74 -      val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
    1.75 +      val _ = trace("\nGot command from parent: " ^ thisLine)
    1.76    in
    1.77       if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
    1.78       else if thisLine = "Kill children\n"
    1.79 @@ -205,13 +192,7 @@
    1.80  	   TextIO.flushOut toParentStr;
    1.81  	   (("","","Kill children",[],"")::cmdList)  )
    1.82       else let val thisCmd = getCmd thisLine 
    1.83 -	       (*********************************************************)
    1.84 -	       (* thisCmd = (prover,proverCmd, settings, file)*)
    1.85 -	       (* i.e. put back into tuple format                       *)
    1.86 -	       (*********************************************************)
    1.87 -	   in
    1.88 -	       getCmds (toParentStr, fromParentStr, thisCmd::cmdList)
    1.89 -	   end
    1.90 +	   in getCmds (toParentStr, fromParentStr, thisCmd::cmdList) end
    1.91    end
    1.92  	    
    1.93                                                                    
    1.94 @@ -251,25 +232,19 @@
    1.95   (*************************************************************)
    1.96   
    1.97   fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = 
    1.98 -   case OS.IO.pollDesc fromParentIOD
    1.99 -   of SOME pd =>
   1.100 -       let val pd' = OS.IO.pollIn pd
   1.101 -	   val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   1.102 -       in
   1.103 -	  if null pdl 
   1.104 -	  then NONE
   1.105 -	  else if OS.IO.isIn (hd pdl)
   1.106 -	       then SOME (getCmds (toParentStr, fromParentStr, []))
   1.107 -	       else NONE
   1.108 -       end
   1.109 +   case OS.IO.pollDesc fromParentIOD of
   1.110 +      SOME pd =>
   1.111 +	 (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
   1.112 +	      [] => NONE
   1.113 +	    | pd''::_ => if OS.IO.isIn pd''
   1.114 +	 	         then SOME (getCmds (toParentStr, fromParentStr, []))
   1.115 +	 	         else NONE)
   1.116     | NONE => NONE;
   1.117  
   1.118  (*get the number of the subgoal from the filename: the last digit string*)
   1.119  fun number_from_filename s =
   1.120    case String.tokens (not o Char.isDigit) s of
   1.121 -      [] => (File.append (File.tmp_path trace_path) 
   1.122 -		    "\nWatcher could not read subgoal nunber!!";
   1.123 -		    raise ERROR)
   1.124 +      [] => (trace "\nWatcher could not read subgoal nunber!!"; raise ERROR)
   1.125      | numbers => valOf (Int.fromString (List.last numbers));
   1.126  
   1.127  fun setupWatcher (thm,clause_arr) = 
   1.128 @@ -292,79 +267,54 @@
   1.129  
   1.130  				      (*************************)
   1.131         | NONE => let                  (* child - i.e. watcher  *)
   1.132 -	   val oldchildin = #infd p1  (*************************)
   1.133 -	   val fromParent = Posix.FileSys.wordToFD 0w0
   1.134 -	   val oldchildout = #outfd p2
   1.135 -	   val toParent = Posix.FileSys.wordToFD 0w1
   1.136 -	   val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   1.137 -	   val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   1.138 -	   val toParentStr = openOutFD ("_exec_out_parent", toParent)
   1.139 -	   val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   1.140 +	  val oldchildin = #infd p1   (*************************)
   1.141 +	  val fromParent = Posix.FileSys.wordToFD 0w0
   1.142 +	  val oldchildout = #outfd p2
   1.143 +	  val toParent = Posix.FileSys.wordToFD 0w1
   1.144 +	  val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   1.145 +	  val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   1.146 +	  val toParentStr = openOutFD ("_exec_out_parent", toParent)
   1.147 +	  val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   1.148  	 
   1.149  	  fun pollChildInput fromStr = 
   1.150 -	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
   1.151 -			 ("\nIn child_poll")
   1.152 -	       val iod = getInIoDesc fromStr
   1.153 -	   in 
   1.154 -	     if isSome iod 
   1.155 -	     then 
   1.156 -	       let val pd = OS.IO.pollDesc (valOf iod)
   1.157 -	       in 
   1.158 -	       if isSome pd then 
   1.159 -		   let val pd' = OS.IO.pollIn (valOf pd)
   1.160 -		       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   1.161 -		   in
   1.162 -		      if null pdl 
   1.163 -		      then
   1.164 -			(File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl\n"; 
   1.165 -			 NONE)
   1.166 -		      else if OS.IO.isIn (hd pdl)
   1.167 -		      then
   1.168 -			   let val inval = TextIO.inputLine fromStr
   1.169 -			       val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
   1.170 -			   in SOME inval end
   1.171 -		      else
   1.172 -                        (File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl \n";
   1.173 -                         NONE)
   1.174 -		   end
   1.175 -		 else NONE
   1.176 -		 end
   1.177 -	     else NONE
   1.178 -	   end
   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 +			  case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
   1.186 +			      [] => false
   1.187 +			    | pd''::_ => OS.IO.isIn pd''
   1.188 +			end
   1.189 +		   | NONE => false)
   1.190 +	     | NONE => false
   1.191  
   1.192 -	(* Check all ATP processes currently running for output                 *)
   1.193 -						   (*********************************)
   1.194 -	 fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   1.195 -						   (*********************************)
   1.196 -	 |   checkChildren ((childProc::otherChildren), toParentStr) = 
   1.197 -	       let val _ = File.append (File.tmp_path trace_path) 
   1.198 -			      ("\nIn check child, length of queue:"^
   1.199 -			        Int.toString (length (childProc::otherChildren)))
   1.200 +
   1.201 +	  (* Check all ATP processes currently running for output                 *)
   1.202 +	  fun checkChildren ([], toParentStr) = []  (* no children to check *)
   1.203 +	  |   checkChildren (childProc::otherChildren, toParentStr) = 
   1.204 +	       let val _ = trace ("\nIn check child, length of queue:"^
   1.205 +			          Int.toString (length (childProc::otherChildren)))
   1.206  		   val (childInput,childOutput) = cmdstreamsOf childProc
   1.207  		   val child_handle = cmdchildHandle childProc
   1.208 -		   (* childCmd is the .dfg file that the problem is in *)
   1.209 +		   (* childCmd is the file that the problem is in *)
   1.210  		   val childCmd = fst(snd (cmdchildInfo childProc))
   1.211 -		   val _ = File.append (File.tmp_path trace_path) 
   1.212 -			      ("\nchildCmd = " ^ childCmd)
   1.213 +		   val _ = trace ("\nchildCmd = " ^ childCmd)
   1.214  		   val sg_num = number_from_filename childCmd
   1.215  		   val childIncoming = pollChildInput childInput
   1.216 -		   val _ = File.append (File.tmp_path trace_path) 
   1.217 -			         "\nfinished polling child"
   1.218  		   val parentID = Posix.ProcEnv.getppid()
   1.219  		   val prover = cmdProver childProc
   1.220  		   val prems_string = prems_string_of thm
   1.221  		   val goalstring = cmdGoal childProc							
   1.222 -		   val _ =  File.append (File.tmp_path trace_path) 
   1.223 -		             ("\nsubgoals forked to checkChildren: " ^ goalstring)
   1.224  	       in 
   1.225 -		 if isSome childIncoming
   1.226 +		 trace("\nsubgoals forked to checkChildren: " ^ goalstring);
   1.227 +		 if childIncoming
   1.228  		 then 
   1.229  		   (* check here for prover label on child*)
   1.230 -		   let val _ = File.append (File.tmp_path trace_path) 
   1.231 -			        ("\nInput available from childIncoming" ^
   1.232 -			         "\nchecking if proof found." ^
   1.233 -			         "\nchildCmd is " ^ childCmd ^ 
   1.234 -			         "\ngoalstring is: " ^ goalstring ^ "\n\n")
   1.235 +		   let val _ = trace ("\nInput available from child: " ^
   1.236 +				      childCmd ^ 
   1.237 +				      "\ngoalstring is " ^ goalstring ^ "\n\n")
   1.238  		       val childDone = (case prover of
   1.239  			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
   1.240  			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
   1.241 @@ -373,19 +323,13 @@
   1.242  		     if childDone
   1.243  		     then (* child has found a proof and transferred it *)
   1.244  			(* Remove this child and go on to check others*)
   1.245 -			(**********************************************)
   1.246  			(Unix.reap child_handle;
   1.247  			 checkChildren(otherChildren, toParentStr))
   1.248 -		     else 
   1.249 -			(**********************************************)
   1.250 -			(* Keep this child and go on to check others  *)
   1.251 -			(**********************************************)
   1.252 -		       (childProc::(checkChildren (otherChildren, toParentStr)))
   1.253 +		     else (* Keep this child and go on to check others  *)
   1.254 +		       childProc :: checkChildren (otherChildren, toParentStr)
   1.255  		  end
   1.256 -		else
   1.257 -		  (File.append (File.tmp_path trace_path)
   1.258 -		               "\nNo child output";
   1.259 -		   childProc::(checkChildren (otherChildren, toParentStr)))
   1.260 +		else (trace "\nNo child output";
   1.261 +		      childProc::(checkChildren (otherChildren, toParentStr)))
   1.262  	       end
   1.263  
   1.264  	
   1.265 @@ -400,15 +344,14 @@
   1.266  (*** add subgoal id num to this *)
   1.267  	fun execCmds  [] procList = procList
   1.268  	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   1.269 -	      let val _ = File.write (File.tmp_path (Path.basic "exec_child"))  
   1.270 +	      let val _ = trace 
   1.271  	                    (space_implode "\n" 
   1.272 -	                      (["About to execute command for goal:",
   1.273 +	                      (["\nAbout to execute command for goal:",
   1.274  	                        goalstring, proverCmd] @ settings @
   1.275  	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   1.276  	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   1.277  		       (Unix.execute(proverCmd, (settings@[file])))
   1.278  		  val (instr, outstr) = Unix.streamsOf childhandle
   1.279 -		  
   1.280  		  val newProcList = (CMDPROC{
   1.281  				       prover = prover,
   1.282  				       cmd = file,
   1.283 @@ -417,12 +360,9 @@
   1.284  				       instr = instr,
   1.285  				       outstr = outstr }) :: procList
   1.286       
   1.287 -		  val _ = File.append (File.tmp_path (Path.basic "exec_child")) 
   1.288 -			    ("\nFinished at " ^
   1.289 -			     Date.toString(Date.fromTimeLocal(Time.now())))
   1.290 -	      in
   1.291 -		execCmds cmds newProcList
   1.292 -	      end
   1.293 +		  val _ = trace ("\nFinished at " ^
   1.294 +			         Date.toString(Date.fromTimeLocal(Time.now())))
   1.295 +	      in execCmds cmds newProcList end
   1.296  
   1.297  
   1.298       (****************************************)                  
   1.299 @@ -446,17 +386,16 @@
   1.300  
   1.301  	 fun keepWatching (procList) = 
   1.302  	   let fun loop procList =  
   1.303 -		let val _ = File.append (File.tmp_path trace_path) 
   1.304 -			       ("\nCalling pollParentInput: " ^ 
   1.305 -			        Int.toString (!iterations_left));
   1.306 +		let val _ = trace ("\nCalling pollParentInput: " ^ 
   1.307 +			           Int.toString (!iterations_left));
   1.308  		    val cmdsFromIsa = pollParentInput 
   1.309  		                       (fromParentIOD, fromParentStr, toParentStr)
   1.310  		in 
   1.311 +		   OS.Process.sleep (Time.fromMilliseconds 100);
   1.312  		   iterations_left := !iterations_left - 1;
   1.313  		   if !iterations_left <= 0 
   1.314 -		   then (*Sadly, this code fails to terminate the watcher!*)
   1.315 -		    (File.append (File.tmp_path trace_path) 
   1.316 -			         "\nTimeout: Killing proof processes";
   1.317 +		   then 
   1.318 +		    (trace "\nTimeout: Killing proof processes";
   1.319  	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   1.320  		     TextIO.flushOut toParentStr;
   1.321  		     killChildren (map cmdchildHandle procList);
   1.322 @@ -476,13 +415,11 @@
   1.323  			 let 
   1.324  			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.325  			   val _ = Posix.ProcEnv.getppid()
   1.326 -			   val _ = File.append (File.tmp_path trace_path)
   1.327 -			      "\nJust execed a child"
   1.328 +			   val _ = trace "\nJust execed a child"
   1.329  			   val newProcList' = checkChildren (newProcList, toParentStr) 
   1.330  			 in
   1.331 -			   File.append (File.tmp_path trace_path) 
   1.332 -			       ("\nOff to keep watching: " ^ 
   1.333 -			        Int.toString (!iterations_left));
   1.334 +			   trace ("\nOff to keep watching: " ^ 
   1.335 +			          Int.toString (!iterations_left));
   1.336  			   loop newProcList'
   1.337  			 end
   1.338  		       else  (* Execute remotely              *)
   1.339 @@ -497,9 +434,8 @@
   1.340  		   else (* No new input from Isabelle *)
   1.341  		     let val newProcList = checkChildren (procList, toParentStr)
   1.342  		     in
   1.343 -		       File.append (File.tmp_path trace_path) 
   1.344 -			       ("\nNo new input, still watching: " ^ 
   1.345 -			        Int.toString (!iterations_left));
   1.346 +		       trace ("\nNo new input, still watching: " ^ 
   1.347 +			      Int.toString (!iterations_left));
   1.348  		       loop newProcList
   1.349  		     end
   1.350  		 end
   1.351 @@ -583,9 +519,8 @@
   1.352  	  (goals_being_watched := !goals_being_watched - 1;
   1.353  	   if !goals_being_watched = 0
   1.354  	   then 
   1.355 -	     (File.append (File.tmp_path (Path.basic "reap_found"))
   1.356 -	       ("Reaping a watcher, childpid = "^
   1.357 -		LargeWord.toString (Posix.Process.pidToWord childpid)^"\n");
   1.358 +	     (trace ("\nReaping a watcher, childpid = "^
   1.359 +		     LargeWord.toString (Posix.Process.pidToWord childpid));
   1.360  	      killWatcher childpid; reapWatcher (childpid,childin, childout))
   1.361  	    else ())
   1.362       val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
   1.363 @@ -597,24 +532,23 @@
   1.364  		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
   1.365         in 
   1.366  	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
   1.367 -	 then (tracing (Recon_Transfer.apply_res_thm outcome goalstring);
   1.368 +	 then (priority (Recon_Transfer.apply_res_thm outcome goalstring);
   1.369  	       decr_watched())
   1.370  	 else if String.isPrefix "Invalid" outcome
   1.371 -	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "is not provable");
   1.372 +	 then (priority (goalstring ^ "is not provable");
   1.373  	       decr_watched())
   1.374  	 else if String.isPrefix "Failure" outcome
   1.375 -	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "proof attempt failed");
   1.376 +	 then (priority (goalstring ^ "proof attempt failed");
   1.377  	       decr_watched()) 
   1.378  	(* print out a list of rules used from clasimpset*)
   1.379  	 else if String.isPrefix "Success" outcome
   1.380 -	 then (tracing (goalstring^outcome);
   1.381 +	 then (priority (goalstring^outcome);
   1.382  	       decr_watched())
   1.383  	  (* if proof translation failed *)
   1.384  	 else if String.isPrefix "Translation failed" outcome
   1.385 -	 then (tracing (goalstring ^ Recon_Transfer.restore_linebreaks outcome);
   1.386 +	 then (priority (goalstring ^ outcome);
   1.387  	       decr_watched())
   1.388 -	 else  
   1.389 -	      (tracing "System error in proof handler";
   1.390 +	 else (priority "System error in proof handler";
   1.391  	       decr_watched())
   1.392         end
   1.393   in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);