removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
authorpaulson
Thu Sep 22 14:09:48 2005 +0200 (2005-09-22)
changeset 17583c272b91b619f
parent 17582 df49216dc592
child 17584 6eab0f1cb0fe
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
src/HOL/Tools/ATP/AtpCommunication.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/watcher.ML
     1.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML	Thu Sep 22 14:02:14 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Thu Sep 22 14:09:48 2005 +0200
     1.3 @@ -87,9 +87,7 @@
     1.4   (TextIO.output (toParent, msg);
     1.5    TextIO.output (toParent, goalstring^"\n");
     1.6    TextIO.flushOut toParent;
     1.7 -  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
     1.8 -  (*Space apart signals arising from multiple subgoals*)
     1.9 -  Posix.Process.sleep(Time.fromMilliseconds 200));
    1.10 +  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
    1.11  
    1.12  (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
    1.13  fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 22 14:02:14 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 22 14:09:48 2005 +0200
     2.3 @@ -301,9 +301,7 @@
     2.4  	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
     2.5  	 TextIO.flushOut toParent;
     2.6  
     2.7 -	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
     2.8 -	(* Attempt to prevent several signals from turning up simultaneously *)
     2.9 -	 Posix.Process.sleep(Time.fromSeconds 1); ()
    2.10 +	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
    2.11      end
    2.12      handle exn => (*FIXME: exn handler is too general!*)
    2.13       (File.write(File.tmp_path (Path.basic "proverString_handler")) 
    2.14 @@ -312,9 +310,7 @@
    2.15                       remove_linebreaks proofstr ^ "\n");
    2.16        TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
    2.17        TextIO.flushOut toParent;
    2.18 -      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    2.19 -      (* Attempt to prevent several signals from turning up simultaneously *)
    2.20 -      Posix.Process.sleep(Time.fromSeconds 1); ());
    2.21 +      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
    2.22  
    2.23  val e_lemma_list = prover_lemma_list_aux get_axiom_names_e;
    2.24  
    2.25 @@ -383,10 +379,8 @@
    2.26         TextIO.output (toParent, reconstr^"\n");
    2.27         TextIO.output (toParent, goalstring^"\n");
    2.28         TextIO.flushOut toParent;
    2.29 -
    2.30         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    2.31 -      (* Attempt to prevent several signals from turning up simultaneously *)
    2.32 -       Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
    2.33 +       all_tac
    2.34    end
    2.35    handle exn => (*FIXME: exn handler is too general!*)
    2.36     (File.append(File.tmp_path (Path.basic "prover_reconstruction"))
    2.37 @@ -395,9 +389,7 @@
    2.38           (remove_linebreaks proofstr) ^"\n");
    2.39      TextIO.output (toParent, goalstring^"\n");
    2.40      TextIO.flushOut toParent;
    2.41 -    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    2.42 -    (* Attempt to prevent several signals from turning up simultaneously *)
    2.43 -    Posix.Process.sleep(Time.fromSeconds 1); all_tac)
    2.44 +    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac)
    2.45  
    2.46  (**********************************************************************************)
    2.47  (* At other end, want to turn back into datatype so can apply reconstruct_proof.  *)
    2.48 @@ -699,10 +691,8 @@
    2.49        val _ = File.append (File.tmp_path (Path.basic "apply_res_1")) 
    2.50  	 ("str is: "^str^" goalstr is: "^goalstring^"\n")	
    2.51        val (frees,recon_steps) = parse_step tokens 
    2.52 -      val isar_str = to_isar_proof (frees, recon_steps, goalstring)
    2.53 -      val foo = File.write (File.tmp_path (Path.basic "apply_res_2")) isar_str
    2.54    in 
    2.55 -     Pretty.writeln(Pretty.str isar_str)
    2.56 +      to_isar_proof (frees, recon_steps, goalstring)
    2.57    end 
    2.58  
    2.59  end;
     3.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Sep 22 14:02:14 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Sep 22 14:09:48 2005 +0200
     3.3 @@ -45,6 +45,9 @@
     3.4  
     3.5  val goals_being_watched = ref 0;
     3.6  
     3.7 +val trace_path = Path.basic "watcher_trace";
     3.8 +
     3.9 +
    3.10  (*  The result of calling createWatcher  *)
    3.11  datatype proc = PROC of {
    3.12          pid : Posix.Process.pid,
    3.13 @@ -261,6 +264,14 @@
    3.14         end
    3.15     | NONE => NONE;
    3.16  
    3.17 +(*get the number of the subgoal from the filename: the last digit string*)
    3.18 +fun number_from_filename s =
    3.19 +  case String.tokens (not o Char.isDigit) s of
    3.20 +      [] => (File.append (File.tmp_path trace_path) 
    3.21 +		    "\nWatcher could not read subgoal nunber!!";
    3.22 +		    raise ERROR)
    3.23 +    | numbers => valOf (Int.fromString (List.last numbers));
    3.24 +
    3.25  fun setupWatcher (thm,clause_arr) = 
    3.26    let
    3.27      (** pipes for communication between parent and watcher **)
    3.28 @@ -292,7 +303,7 @@
    3.29  	 
    3.30  	  fun pollChildInput fromStr = 
    3.31  	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
    3.32 -			 ("In child_poll\n")
    3.33 +			 ("\nIn child_poll")
    3.34  	       val iod = getInIoDesc fromStr
    3.35  	   in 
    3.36  	     if isSome iod 
    3.37 @@ -321,52 +332,35 @@
    3.38  	     else NONE
    3.39  	   end
    3.40  
    3.41 -         val cc_iterations_left = ref 50;  
    3.42 -         (*FIXME: why does this loop if not explicitly bounded?*)
    3.43 -
    3.44  	(* Check all ATP processes currently running for output                 *)
    3.45  						   (*********************************)
    3.46  	 fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
    3.47  						   (*********************************)
    3.48  	 |   checkChildren ((childProc::otherChildren), toParentStr) = 
    3.49 -	       let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
    3.50 -			      ("In check child, length of queue:"^
    3.51 -			        Int.toString (length (childProc::otherChildren)) ^
    3.52 -			       "\niterations left = " ^ Int.toString (!cc_iterations_left))
    3.53 -		   val _ = Posix.Process.sleep (Time.fromMilliseconds 50) (*slow the looping*)
    3.54 +	       let val _ = File.append (File.tmp_path trace_path) 
    3.55 +			      ("\nIn check child, length of queue:"^
    3.56 +			        Int.toString (length (childProc::otherChildren)))
    3.57  		   val (childInput,childOutput) = cmdstreamsOf childProc
    3.58  		   val child_handle = cmdchildHandle childProc
    3.59  		   (* childCmd is the .dfg file that the problem is in *)
    3.60  		   val childCmd = fst(snd (cmdchildInfo childProc))
    3.61 -		   val _ = File.append (File.tmp_path (Path.basic "child_check")) 
    3.62 +		   val _ = File.append (File.tmp_path trace_path) 
    3.63  			      ("\nchildCmd = " ^ childCmd)
    3.64 -		   (* now get the number of the subgoal from the filename *)
    3.65 -		   val path_parts = String.tokens(fn c => c = #"/") childCmd
    3.66 -		   val digits = String.translate 
    3.67 -		                  (fn c => if Char.isDigit c then str c else "")
    3.68 -		                  (List.last path_parts);
    3.69 -		   val sg_num =
    3.70 -		     (case Int.fromString digits of SOME n => n
    3.71 -                        | NONE => (File.append (File.tmp_path (Path.basic "child_check")) 
    3.72 -                                   "\nWatcher could not read subgoal nunber!!";
    3.73 -                                   raise ERROR));
    3.74 +		   val sg_num = number_from_filename childCmd
    3.75  		   val childIncoming = pollChildInput childInput
    3.76 -		   val _ = File.append (File.tmp_path (Path.basic "child_check")) 
    3.77 +		   val _ = File.append (File.tmp_path trace_path) 
    3.78  			         "\nfinished polling child"
    3.79  		   val parentID = Posix.ProcEnv.getppid()
    3.80  		   val prover = cmdProver childProc
    3.81  		   val prems_string = prems_string_of thm
    3.82  		   val goalstring = cmdGoal childProc							
    3.83 -		   val _ =  File.append (File.tmp_path (Path.basic "child_check")) 
    3.84 -		             ("\nsubgoals forked to checkChildren: " ^ 
    3.85 -		              space_implode "\n" [prems_string,prover,goalstring])
    3.86 +		   val _ =  File.append (File.tmp_path trace_path) 
    3.87 +		             ("\nsubgoals forked to checkChildren: " ^ goalstring)
    3.88  	       in 
    3.89 -	         cc_iterations_left := !cc_iterations_left - 1;
    3.90 -		 if !cc_iterations_left = 0 then [] (*Abandon looping!*)
    3.91 -		 else if isSome childIncoming
    3.92 +		 if isSome childIncoming
    3.93  		 then 
    3.94  		   (* check here for prover label on child*)
    3.95 -		   let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
    3.96 +		   let val _ = File.append (File.tmp_path trace_path) 
    3.97  			        ("\nInput available from childIncoming" ^
    3.98  			         "\nchecking if proof found." ^
    3.99  			         "\nchildCmd is " ^ childCmd ^ 
   3.100 @@ -389,8 +383,8 @@
   3.101  		       (childProc::(checkChildren (otherChildren, toParentStr)))
   3.102  		  end
   3.103  		else
   3.104 -		  (File.append (File.tmp_path (Path.basic "child_check"))
   3.105 -		               "No child output";
   3.106 +		  (File.append (File.tmp_path trace_path)
   3.107 +		               "\nNo child output";
   3.108  		   childProc::(checkChildren (otherChildren, toParentStr)))
   3.109  	       end
   3.110  
   3.111 @@ -427,7 +421,6 @@
   3.112  			    ("\nFinished at " ^
   3.113  			     Date.toString(Date.fromTimeLocal(Time.now())))
   3.114  	      in
   3.115 -		Posix.Process.sleep (Time.fromSeconds 1); 
   3.116  		execCmds cmds newProcList
   3.117  	      end
   3.118  
   3.119 @@ -449,12 +442,11 @@
   3.120       (**********************************************)                  
   3.121       (* Watcher Loop                               *)
   3.122       (**********************************************)
   3.123 -         val iterations_left = ref 100;  (*don't let it run forever*)
   3.124 +         val iterations_left = ref 500;  (*don't let it run forever*)
   3.125  
   3.126  	 fun keepWatching (procList) = 
   3.127  	   let fun loop procList =  
   3.128 -		let val _ = Posix.Process.sleep (Time.fromMilliseconds 200)
   3.129 -		    val _ = File.append (File.tmp_path (Path.basic "keep_watch")) 
   3.130 +		let val _ = File.append (File.tmp_path trace_path) 
   3.131  			       ("\nCalling pollParentInput: " ^ 
   3.132  			        Int.toString (!iterations_left));
   3.133  		    val cmdsFromIsa = pollParentInput 
   3.134 @@ -463,11 +455,12 @@
   3.135  		   iterations_left := !iterations_left - 1;
   3.136  		   if !iterations_left <= 0 
   3.137  		   then (*Sadly, this code fails to terminate the watcher!*)
   3.138 -		    (File.append (File.tmp_path (Path.basic "keep_watch")) 
   3.139 +		    (File.append (File.tmp_path trace_path) 
   3.140  			         "\nTimeout: Killing proof processes";
   3.141  	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   3.142  		     TextIO.flushOut toParentStr;
   3.143 -		     killChildren (map cmdchildHandle procList))
   3.144 +		     killChildren (map cmdchildHandle procList);
   3.145 +		     exit 0)
   3.146  		   else if isSome cmdsFromIsa
   3.147  		   then (*  deal with input from Isabelle *)
   3.148  		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
   3.149 @@ -483,11 +476,11 @@
   3.150  			 let 
   3.151  			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   3.152  			   val _ = Posix.ProcEnv.getppid()
   3.153 -			   val _ = File.append (File.tmp_path (Path.basic "keep_watch"))
   3.154 +			   val _ = File.append (File.tmp_path trace_path)
   3.155  			      "\nJust execed a child"
   3.156  			   val newProcList' = checkChildren (newProcList, toParentStr) 
   3.157  			 in
   3.158 -			   File.append (File.tmp_path (Path.basic "keep_watch")) 
   3.159 +			   File.append (File.tmp_path trace_path) 
   3.160  			       ("\nOff to keep watching: " ^ 
   3.161  			        Int.toString (!iterations_left));
   3.162  			   loop newProcList'
   3.163 @@ -504,7 +497,7 @@
   3.164  		   else (* No new input from Isabelle *)
   3.165  		     let val newProcList = checkChildren (procList, toParentStr)
   3.166  		     in
   3.167 -		       File.append (File.tmp_path (Path.basic "keep_watch")) 
   3.168 +		       File.append (File.tmp_path trace_path) 
   3.169  			       ("\nNo new input, still watching: " ^ 
   3.170  			        Int.toString (!iterations_left));
   3.171  		       loop newProcList
   3.172 @@ -604,38 +597,24 @@
   3.173  		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
   3.174         in 
   3.175  	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
   3.176 -	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   3.177 -	       Recon_Transfer.apply_res_thm outcome goalstring;
   3.178 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   3.179 +	 then (tracing (Recon_Transfer.apply_res_thm outcome goalstring);
   3.180  	       decr_watched())
   3.181  	 else if String.isPrefix "Invalid" outcome
   3.182 -	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   3.183 -	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) 
   3.184 -	       ^ "is not provable"));
   3.185 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   3.186 +	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "is not provable");
   3.187  	       decr_watched())
   3.188  	 else if String.isPrefix "Failure" outcome
   3.189 -	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   3.190 -	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) 
   3.191 -	       ^ "proof attempt failed"));
   3.192 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   3.193 +	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "proof attempt failed");
   3.194  	       decr_watched()) 
   3.195  	(* print out a list of rules used from clasimpset*)
   3.196  	 else if String.isPrefix "Success" outcome
   3.197 -	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   3.198 -	       Pretty.writeln(Pretty.str (goalstring^outcome));
   3.199 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   3.200 +	 then (tracing (goalstring^outcome);
   3.201  	       decr_watched())
   3.202  	  (* if proof translation failed *)
   3.203  	 else if String.isPrefix "Translation failed" outcome
   3.204 -	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   3.205 -	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks outcome)));
   3.206 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   3.207 +	 then (tracing (goalstring ^ Recon_Transfer.restore_linebreaks outcome);
   3.208  	       decr_watched())
   3.209  	 else  
   3.210 -	      (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   3.211 -	       Pretty.writeln(Pretty.str ("System error in proof handler"));
   3.212 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   3.213 +	      (tracing "System error in proof handler";
   3.214  	       decr_watched())
   3.215         end
   3.216   in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);