src/HOL/Tools/ATP/watcher.ML
changeset 17583 c272b91b619f
parent 17568 e93f7510e1e1
child 17690 8ba7c3cd24a8
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Sep 22 14:02:14 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Sep 22 14:09:48 2005 +0200
     1.3 @@ -45,6 +45,9 @@
     1.4  
     1.5  val goals_being_watched = ref 0;
     1.6  
     1.7 +val trace_path = Path.basic "watcher_trace";
     1.8 +
     1.9 +
    1.10  (*  The result of calling createWatcher  *)
    1.11  datatype proc = PROC of {
    1.12          pid : Posix.Process.pid,
    1.13 @@ -261,6 +264,14 @@
    1.14         end
    1.15     | NONE => NONE;
    1.16  
    1.17 +(*get the number of the subgoal from the filename: the last digit string*)
    1.18 +fun number_from_filename s =
    1.19 +  case String.tokens (not o Char.isDigit) s of
    1.20 +      [] => (File.append (File.tmp_path trace_path) 
    1.21 +		    "\nWatcher could not read subgoal nunber!!";
    1.22 +		    raise ERROR)
    1.23 +    | numbers => valOf (Int.fromString (List.last numbers));
    1.24 +
    1.25  fun setupWatcher (thm,clause_arr) = 
    1.26    let
    1.27      (** pipes for communication between parent and watcher **)
    1.28 @@ -292,7 +303,7 @@
    1.29  	 
    1.30  	  fun pollChildInput fromStr = 
    1.31  	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
    1.32 -			 ("In child_poll\n")
    1.33 +			 ("\nIn child_poll")
    1.34  	       val iod = getInIoDesc fromStr
    1.35  	   in 
    1.36  	     if isSome iod 
    1.37 @@ -321,52 +332,35 @@
    1.38  	     else NONE
    1.39  	   end
    1.40  
    1.41 -         val cc_iterations_left = ref 50;  
    1.42 -         (*FIXME: why does this loop if not explicitly bounded?*)
    1.43 -
    1.44  	(* Check all ATP processes currently running for output                 *)
    1.45  						   (*********************************)
    1.46  	 fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
    1.47  						   (*********************************)
    1.48  	 |   checkChildren ((childProc::otherChildren), toParentStr) = 
    1.49 -	       let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
    1.50 -			      ("In check child, length of queue:"^
    1.51 -			        Int.toString (length (childProc::otherChildren)) ^
    1.52 -			       "\niterations left = " ^ Int.toString (!cc_iterations_left))
    1.53 -		   val _ = Posix.Process.sleep (Time.fromMilliseconds 50) (*slow the looping*)
    1.54 +	       let val _ = File.append (File.tmp_path trace_path) 
    1.55 +			      ("\nIn check child, length of queue:"^
    1.56 +			        Int.toString (length (childProc::otherChildren)))
    1.57  		   val (childInput,childOutput) = cmdstreamsOf childProc
    1.58  		   val child_handle = cmdchildHandle childProc
    1.59  		   (* childCmd is the .dfg file that the problem is in *)
    1.60  		   val childCmd = fst(snd (cmdchildInfo childProc))
    1.61 -		   val _ = File.append (File.tmp_path (Path.basic "child_check")) 
    1.62 +		   val _ = File.append (File.tmp_path trace_path) 
    1.63  			      ("\nchildCmd = " ^ childCmd)
    1.64 -		   (* now get the number of the subgoal from the filename *)
    1.65 -		   val path_parts = String.tokens(fn c => c = #"/") childCmd
    1.66 -		   val digits = String.translate 
    1.67 -		                  (fn c => if Char.isDigit c then str c else "")
    1.68 -		                  (List.last path_parts);
    1.69 -		   val sg_num =
    1.70 -		     (case Int.fromString digits of SOME n => n
    1.71 -                        | NONE => (File.append (File.tmp_path (Path.basic "child_check")) 
    1.72 -                                   "\nWatcher could not read subgoal nunber!!";
    1.73 -                                   raise ERROR));
    1.74 +		   val sg_num = number_from_filename childCmd
    1.75  		   val childIncoming = pollChildInput childInput
    1.76 -		   val _ = File.append (File.tmp_path (Path.basic "child_check")) 
    1.77 +		   val _ = File.append (File.tmp_path trace_path) 
    1.78  			         "\nfinished polling child"
    1.79  		   val parentID = Posix.ProcEnv.getppid()
    1.80  		   val prover = cmdProver childProc
    1.81  		   val prems_string = prems_string_of thm
    1.82  		   val goalstring = cmdGoal childProc							
    1.83 -		   val _ =  File.append (File.tmp_path (Path.basic "child_check")) 
    1.84 -		             ("\nsubgoals forked to checkChildren: " ^ 
    1.85 -		              space_implode "\n" [prems_string,prover,goalstring])
    1.86 +		   val _ =  File.append (File.tmp_path trace_path) 
    1.87 +		             ("\nsubgoals forked to checkChildren: " ^ goalstring)
    1.88  	       in 
    1.89 -	         cc_iterations_left := !cc_iterations_left - 1;
    1.90 -		 if !cc_iterations_left = 0 then [] (*Abandon looping!*)
    1.91 -		 else if isSome childIncoming
    1.92 +		 if isSome childIncoming
    1.93  		 then 
    1.94  		   (* check here for prover label on child*)
    1.95 -		   let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
    1.96 +		   let val _ = File.append (File.tmp_path trace_path) 
    1.97  			        ("\nInput available from childIncoming" ^
    1.98  			         "\nchecking if proof found." ^
    1.99  			         "\nchildCmd is " ^ childCmd ^ 
   1.100 @@ -389,8 +383,8 @@
   1.101  		       (childProc::(checkChildren (otherChildren, toParentStr)))
   1.102  		  end
   1.103  		else
   1.104 -		  (File.append (File.tmp_path (Path.basic "child_check"))
   1.105 -		               "No child output";
   1.106 +		  (File.append (File.tmp_path trace_path)
   1.107 +		               "\nNo child output";
   1.108  		   childProc::(checkChildren (otherChildren, toParentStr)))
   1.109  	       end
   1.110  
   1.111 @@ -427,7 +421,6 @@
   1.112  			    ("\nFinished at " ^
   1.113  			     Date.toString(Date.fromTimeLocal(Time.now())))
   1.114  	      in
   1.115 -		Posix.Process.sleep (Time.fromSeconds 1); 
   1.116  		execCmds cmds newProcList
   1.117  	      end
   1.118  
   1.119 @@ -449,12 +442,11 @@
   1.120       (**********************************************)                  
   1.121       (* Watcher Loop                               *)
   1.122       (**********************************************)
   1.123 -         val iterations_left = ref 100;  (*don't let it run forever*)
   1.124 +         val iterations_left = ref 500;  (*don't let it run forever*)
   1.125  
   1.126  	 fun keepWatching (procList) = 
   1.127  	   let fun loop procList =  
   1.128 -		let val _ = Posix.Process.sleep (Time.fromMilliseconds 200)
   1.129 -		    val _ = File.append (File.tmp_path (Path.basic "keep_watch")) 
   1.130 +		let val _ = File.append (File.tmp_path trace_path) 
   1.131  			       ("\nCalling pollParentInput: " ^ 
   1.132  			        Int.toString (!iterations_left));
   1.133  		    val cmdsFromIsa = pollParentInput 
   1.134 @@ -463,11 +455,12 @@
   1.135  		   iterations_left := !iterations_left - 1;
   1.136  		   if !iterations_left <= 0 
   1.137  		   then (*Sadly, this code fails to terminate the watcher!*)
   1.138 -		    (File.append (File.tmp_path (Path.basic "keep_watch")) 
   1.139 +		    (File.append (File.tmp_path trace_path) 
   1.140  			         "\nTimeout: Killing proof processes";
   1.141  	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   1.142  		     TextIO.flushOut toParentStr;
   1.143 -		     killChildren (map cmdchildHandle procList))
   1.144 +		     killChildren (map cmdchildHandle procList);
   1.145 +		     exit 0)
   1.146  		   else if isSome cmdsFromIsa
   1.147  		   then (*  deal with input from Isabelle *)
   1.148  		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
   1.149 @@ -483,11 +476,11 @@
   1.150  			 let 
   1.151  			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.152  			   val _ = Posix.ProcEnv.getppid()
   1.153 -			   val _ = File.append (File.tmp_path (Path.basic "keep_watch"))
   1.154 +			   val _ = File.append (File.tmp_path trace_path)
   1.155  			      "\nJust execed a child"
   1.156  			   val newProcList' = checkChildren (newProcList, toParentStr) 
   1.157  			 in
   1.158 -			   File.append (File.tmp_path (Path.basic "keep_watch")) 
   1.159 +			   File.append (File.tmp_path trace_path) 
   1.160  			       ("\nOff to keep watching: " ^ 
   1.161  			        Int.toString (!iterations_left));
   1.162  			   loop newProcList'
   1.163 @@ -504,7 +497,7 @@
   1.164  		   else (* No new input from Isabelle *)
   1.165  		     let val newProcList = checkChildren (procList, toParentStr)
   1.166  		     in
   1.167 -		       File.append (File.tmp_path (Path.basic "keep_watch")) 
   1.168 +		       File.append (File.tmp_path trace_path) 
   1.169  			       ("\nNo new input, still watching: " ^ 
   1.170  			        Int.toString (!iterations_left));
   1.171  		       loop newProcList
   1.172 @@ -604,38 +597,24 @@
   1.173  		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
   1.174         in 
   1.175  	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
   1.176 -	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.177 -	       Recon_Transfer.apply_res_thm outcome goalstring;
   1.178 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.179 +	 then (tracing (Recon_Transfer.apply_res_thm outcome goalstring);
   1.180  	       decr_watched())
   1.181  	 else if String.isPrefix "Invalid" outcome
   1.182 -	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.183 -	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) 
   1.184 -	       ^ "is not provable"));
   1.185 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.186 +	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "is not provable");
   1.187  	       decr_watched())
   1.188  	 else if String.isPrefix "Failure" outcome
   1.189 -	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.190 -	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) 
   1.191 -	       ^ "proof attempt failed"));
   1.192 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.193 +	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "proof attempt failed");
   1.194  	       decr_watched()) 
   1.195  	(* print out a list of rules used from clasimpset*)
   1.196  	 else if String.isPrefix "Success" outcome
   1.197 -	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.198 -	       Pretty.writeln(Pretty.str (goalstring^outcome));
   1.199 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.200 +	 then (tracing (goalstring^outcome);
   1.201  	       decr_watched())
   1.202  	  (* if proof translation failed *)
   1.203  	 else if String.isPrefix "Translation failed" outcome
   1.204 -	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.205 -	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks outcome)));
   1.206 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.207 +	 then (tracing (goalstring ^ Recon_Transfer.restore_linebreaks outcome);
   1.208  	       decr_watched())
   1.209  	 else  
   1.210 -	      (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.211 -	       Pretty.writeln(Pretty.str ("System error in proof handler"));
   1.212 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.213 +	      (tracing "System error in proof handler";
   1.214  	       decr_watched())
   1.215         end
   1.216   in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);