time limit option; fixed bug concerning first line of ATP output
authorpaulson
Wed Sep 28 11:16:27 2005 +0200 (2005-09-28)
changeset 176908ba7c3cd24a8
parent 17689 a04b5b43625e
child 17691 8cc72452695c
time limit option; fixed bug concerning first line of ATP output
src/HOL/Tools/ATP/AtpCommunication.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML	Wed Sep 28 11:15:33 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Wed Sep 28 11:16:27 2005 +0200
     1.3 @@ -103,9 +103,8 @@
     1.4         startTransfer (end_V8, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
     1.5       else if (String.isPrefix "Satisfiability detected" thisLine) orelse
     1.6               (String.isPrefix "Refutation not found" thisLine)
     1.7 -     then
     1.8 -       (signal_parent (toParent, ppid, "Failure\n", goalstring);
     1.9 -	true)
    1.10 +     then (signal_parent (toParent, ppid, "Failure\n", goalstring);
    1.11 +	   true)
    1.12       else
    1.13          checkVampProofFound  (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
    1.14    end
    1.15 @@ -124,13 +123,11 @@
    1.16       then      
    1.17         startTransfer (end_E, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
    1.18       else if String.isPrefix "# Problem is satisfiable" thisLine
    1.19 -     then  
    1.20 -       (signal_parent (toParent, ppid, "Invalid\n", goalstring);
    1.21 -	true)
    1.22 -     else if String.isPrefix "# Failure: Resource limit exceeded" thisLine
    1.23 -     then  (*In fact, E distingishes "out of time" and "out of memory"*)
    1.24 -       (signal_parent (toParent, ppid, "Failure\n", goalstring);
    1.25 -	true)
    1.26 +     then (signal_parent (toParent, ppid, "Invalid\n", goalstring);
    1.27 +	   true)
    1.28 +     else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
    1.29 +     then (signal_parent (toParent, ppid, "Failure\n", goalstring);
    1.30 +	   true)
    1.31       else
    1.32  	checkEProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
    1.33   end
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 28 11:15:33 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 28 11:16:27 2005 +0200
     2.3 @@ -147,8 +147,6 @@
     2.4  fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) step_nums = 
     2.5      let val clasimp_nums = List.filter (is_clasimp_ax (Array.length clause_arr - 1)) 
     2.6  	                   (map subone step_nums)
     2.7 -(*	val _ = File.write (File.tmp_path (Path.basic "axnums")) 
     2.8 -                     (numstr clasimp_nums) *)
     2.9      in
    2.10  	map (fn x =>  Array.sub(clause_arr, x)) clasimp_nums
    2.11      end
    2.12 @@ -169,8 +167,6 @@
    2.13    
    2.14        val clasimp_names_cls = get_clasimp_cls clause_arr step_nums 
    2.15        val clasimp_names = map (ResClause.get_axiomName o #1) clasimp_names_cls
    2.16 -      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    2.17 -                         (concat clasimp_names)
    2.18        val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    2.19     in
    2.20        clasimp_names
     3.1 --- a/src/HOL/Tools/ATP/watcher.ML	Wed Sep 28 11:15:33 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Sep 28 11:16:27 2005 +0200
     3.3 @@ -47,6 +47,8 @@
     3.4  
     3.5  val trace_path = Path.basic "watcher_trace";
     3.6  
     3.7 +fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
     3.8 +              else ();
     3.9  
    3.10  (*  The result of calling createWatcher  *)
    3.11  datatype proc = PROC of {
    3.12 @@ -139,9 +141,9 @@
    3.13  |   callResProvers (toWatcherStr,
    3.14                      (prover,goalstring, proverCmd,settings, 
    3.15                       probfile)  ::  args) =
    3.16 -      let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
    3.17 -                             (prover^goalstring^proverCmd^settings^
    3.18 -                              probfile)
    3.19 +      let val _ = trace (space_implode "\n" 
    3.20 +		         (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
    3.21 +			  probfile]))
    3.22        in TextIO.output (toWatcherStr,    
    3.23              (prover^"$"^goalstring^"$"^proverCmd^"$"^
    3.24               settings^"$"^probfile^"\n"));
    3.25 @@ -160,44 +162,29 @@
    3.26                              TextIO.flushOut toWatcherStr)
    3.27  
    3.28  
    3.29 -
    3.30  (**************************************************************)
    3.31  (* Remove \n token from a vampire goal filename and extract   *)
    3.32  (* prover, proverCmd, settings and file from input string     *)
    3.33  (**************************************************************)
    3.34  
    3.35 -fun separateFields str =
    3.36 -  let val _ = File.append (File.tmp_path (Path.basic "sep_field"))
    3.37 -                          ("In separateFields, str is: " ^ str ^ "\n\n") 
    3.38 -      val [prover,goalstring,proverCmd,settingstr,probfile] = 
    3.39 -          String.tokens (fn c => c = #"$") str
    3.40 -      val settings = String.tokens (fn c => c = #"%") settingstr
    3.41 -      val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
    3.42 -                  ("Sep comms are: "^ str ^"**"^
    3.43 -                   prover^" goalstr:  "^goalstring^
    3.44 -                   "\n provercmd: "^proverCmd^
    3.45 -                   "\n prob  "^probfile^"\n\n")
    3.46 -  in
    3.47 -     (prover,goalstring, proverCmd, settings, probfile)
    3.48 -  end
    3.49 -
    3.50  val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
    3.51  
    3.52  fun getCmd cmdStr = 
    3.53 -  let val cmdStr' = remove_newlines cmdStr
    3.54 -  in
    3.55 -      File.write (File.tmp_path (Path.basic"sepfields_call")) 
    3.56 -		 ("about to call separateFields with " ^ cmdStr');
    3.57 -      separateFields cmdStr'
    3.58 -  end;
    3.59 +  let val [prover,goalstring,proverCmd,settingstr,probfile] = 
    3.60 +            String.tokens (fn c => c = #"$") (remove_newlines cmdStr)
    3.61 +      val settings = String.tokens (fn c => c = #"%") settingstr
    3.62 +      val _ = trace ("getCmd: " ^ cmdStr ^
    3.63 +		    "\nprover" ^ prover ^ " goalstr:  "^goalstring^
    3.64 +		    "\nprovercmd: " ^ proverCmd^
    3.65 +		    "\nprob  " ^ probfile ^ "\n\n")
    3.66 +  in (prover,goalstring, proverCmd, settings, probfile) end
    3.67                        
    3.68  (**************************************************************)
    3.69  (* Get commands from Isabelle                                 *)
    3.70  (**************************************************************)
    3.71 -
    3.72  fun getCmds (toParentStr,fromParentStr, cmdList) = 
    3.73    let val thisLine = TextIO.inputLine fromParentStr 
    3.74 -      val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
    3.75 +      val _ = trace("\nGot command from parent: " ^ thisLine)
    3.76    in
    3.77       if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
    3.78       else if thisLine = "Kill children\n"
    3.79 @@ -205,13 +192,7 @@
    3.80  	   TextIO.flushOut toParentStr;
    3.81  	   (("","","Kill children",[],"")::cmdList)  )
    3.82       else let val thisCmd = getCmd thisLine 
    3.83 -	       (*********************************************************)
    3.84 -	       (* thisCmd = (prover,proverCmd, settings, file)*)
    3.85 -	       (* i.e. put back into tuple format                       *)
    3.86 -	       (*********************************************************)
    3.87 -	   in
    3.88 -	       getCmds (toParentStr, fromParentStr, thisCmd::cmdList)
    3.89 -	   end
    3.90 +	   in getCmds (toParentStr, fromParentStr, thisCmd::cmdList) end
    3.91    end
    3.92  	    
    3.93                                                                    
    3.94 @@ -251,25 +232,19 @@
    3.95   (*************************************************************)
    3.96   
    3.97   fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = 
    3.98 -   case OS.IO.pollDesc fromParentIOD
    3.99 -   of SOME pd =>
   3.100 -       let val pd' = OS.IO.pollIn pd
   3.101 -	   val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   3.102 -       in
   3.103 -	  if null pdl 
   3.104 -	  then NONE
   3.105 -	  else if OS.IO.isIn (hd pdl)
   3.106 -	       then SOME (getCmds (toParentStr, fromParentStr, []))
   3.107 -	       else NONE
   3.108 -       end
   3.109 +   case OS.IO.pollDesc fromParentIOD of
   3.110 +      SOME pd =>
   3.111 +	 (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
   3.112 +	      [] => NONE
   3.113 +	    | pd''::_ => if OS.IO.isIn pd''
   3.114 +	 	         then SOME (getCmds (toParentStr, fromParentStr, []))
   3.115 +	 	         else NONE)
   3.116     | NONE => NONE;
   3.117  
   3.118  (*get the number of the subgoal from the filename: the last digit string*)
   3.119  fun number_from_filename s =
   3.120    case String.tokens (not o Char.isDigit) s of
   3.121 -      [] => (File.append (File.tmp_path trace_path) 
   3.122 -		    "\nWatcher could not read subgoal nunber!!";
   3.123 -		    raise ERROR)
   3.124 +      [] => (trace "\nWatcher could not read subgoal nunber!!"; raise ERROR)
   3.125      | numbers => valOf (Int.fromString (List.last numbers));
   3.126  
   3.127  fun setupWatcher (thm,clause_arr) = 
   3.128 @@ -292,79 +267,54 @@
   3.129  
   3.130  				      (*************************)
   3.131         | NONE => let                  (* child - i.e. watcher  *)
   3.132 -	   val oldchildin = #infd p1  (*************************)
   3.133 -	   val fromParent = Posix.FileSys.wordToFD 0w0
   3.134 -	   val oldchildout = #outfd p2
   3.135 -	   val toParent = Posix.FileSys.wordToFD 0w1
   3.136 -	   val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   3.137 -	   val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   3.138 -	   val toParentStr = openOutFD ("_exec_out_parent", toParent)
   3.139 -	   val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   3.140 +	  val oldchildin = #infd p1   (*************************)
   3.141 +	  val fromParent = Posix.FileSys.wordToFD 0w0
   3.142 +	  val oldchildout = #outfd p2
   3.143 +	  val toParent = Posix.FileSys.wordToFD 0w1
   3.144 +	  val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   3.145 +	  val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   3.146 +	  val toParentStr = openOutFD ("_exec_out_parent", toParent)
   3.147 +	  val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   3.148  	 
   3.149  	  fun pollChildInput fromStr = 
   3.150 -	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
   3.151 -			 ("\nIn child_poll")
   3.152 -	       val iod = getInIoDesc fromStr
   3.153 -	   in 
   3.154 -	     if isSome iod 
   3.155 -	     then 
   3.156 -	       let val pd = OS.IO.pollDesc (valOf iod)
   3.157 -	       in 
   3.158 -	       if isSome pd then 
   3.159 -		   let val pd' = OS.IO.pollIn (valOf pd)
   3.160 -		       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   3.161 -		   in
   3.162 -		      if null pdl 
   3.163 -		      then
   3.164 -			(File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl\n"; 
   3.165 -			 NONE)
   3.166 -		      else if OS.IO.isIn (hd pdl)
   3.167 -		      then
   3.168 -			   let val inval = TextIO.inputLine fromStr
   3.169 -			       val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
   3.170 -			   in SOME inval end
   3.171 -		      else
   3.172 -                        (File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl \n";
   3.173 -                         NONE)
   3.174 -		   end
   3.175 -		 else NONE
   3.176 -		 end
   3.177 -	     else NONE
   3.178 -	   end
   3.179 +	     case getInIoDesc fromStr of
   3.180 +	       SOME iod => 
   3.181 +		 (case OS.IO.pollDesc iod of
   3.182 +		    SOME pd =>
   3.183 +			let val pd' = OS.IO.pollIn pd
   3.184 +			in
   3.185 +			  case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
   3.186 +			      [] => false
   3.187 +			    | pd''::_ => OS.IO.isIn pd''
   3.188 +			end
   3.189 +		   | NONE => false)
   3.190 +	     | NONE => false
   3.191  
   3.192 -	(* Check all ATP processes currently running for output                 *)
   3.193 -						   (*********************************)
   3.194 -	 fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   3.195 -						   (*********************************)
   3.196 -	 |   checkChildren ((childProc::otherChildren), toParentStr) = 
   3.197 -	       let val _ = File.append (File.tmp_path trace_path) 
   3.198 -			      ("\nIn check child, length of queue:"^
   3.199 -			        Int.toString (length (childProc::otherChildren)))
   3.200 +
   3.201 +	  (* Check all ATP processes currently running for output                 *)
   3.202 +	  fun checkChildren ([], toParentStr) = []  (* no children to check *)
   3.203 +	  |   checkChildren (childProc::otherChildren, toParentStr) = 
   3.204 +	       let val _ = trace ("\nIn check child, length of queue:"^
   3.205 +			          Int.toString (length (childProc::otherChildren)))
   3.206  		   val (childInput,childOutput) = cmdstreamsOf childProc
   3.207  		   val child_handle = cmdchildHandle childProc
   3.208 -		   (* childCmd is the .dfg file that the problem is in *)
   3.209 +		   (* childCmd is the file that the problem is in *)
   3.210  		   val childCmd = fst(snd (cmdchildInfo childProc))
   3.211 -		   val _ = File.append (File.tmp_path trace_path) 
   3.212 -			      ("\nchildCmd = " ^ childCmd)
   3.213 +		   val _ = trace ("\nchildCmd = " ^ childCmd)
   3.214  		   val sg_num = number_from_filename childCmd
   3.215  		   val childIncoming = pollChildInput childInput
   3.216 -		   val _ = File.append (File.tmp_path trace_path) 
   3.217 -			         "\nfinished polling child"
   3.218  		   val parentID = Posix.ProcEnv.getppid()
   3.219  		   val prover = cmdProver childProc
   3.220  		   val prems_string = prems_string_of thm
   3.221  		   val goalstring = cmdGoal childProc							
   3.222 -		   val _ =  File.append (File.tmp_path trace_path) 
   3.223 -		             ("\nsubgoals forked to checkChildren: " ^ goalstring)
   3.224  	       in 
   3.225 -		 if isSome childIncoming
   3.226 +		 trace("\nsubgoals forked to checkChildren: " ^ goalstring);
   3.227 +		 if childIncoming
   3.228  		 then 
   3.229  		   (* check here for prover label on child*)
   3.230 -		   let val _ = File.append (File.tmp_path trace_path) 
   3.231 -			        ("\nInput available from childIncoming" ^
   3.232 -			         "\nchecking if proof found." ^
   3.233 -			         "\nchildCmd is " ^ childCmd ^ 
   3.234 -			         "\ngoalstring is: " ^ goalstring ^ "\n\n")
   3.235 +		   let val _ = trace ("\nInput available from child: " ^
   3.236 +				      childCmd ^ 
   3.237 +				      "\ngoalstring is " ^ goalstring ^ "\n\n")
   3.238  		       val childDone = (case prover of
   3.239  			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
   3.240  			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
   3.241 @@ -373,19 +323,13 @@
   3.242  		     if childDone
   3.243  		     then (* child has found a proof and transferred it *)
   3.244  			(* Remove this child and go on to check others*)
   3.245 -			(**********************************************)
   3.246  			(Unix.reap child_handle;
   3.247  			 checkChildren(otherChildren, toParentStr))
   3.248 -		     else 
   3.249 -			(**********************************************)
   3.250 -			(* Keep this child and go on to check others  *)
   3.251 -			(**********************************************)
   3.252 -		       (childProc::(checkChildren (otherChildren, toParentStr)))
   3.253 +		     else (* Keep this child and go on to check others  *)
   3.254 +		       childProc :: checkChildren (otherChildren, toParentStr)
   3.255  		  end
   3.256 -		else
   3.257 -		  (File.append (File.tmp_path trace_path)
   3.258 -		               "\nNo child output";
   3.259 -		   childProc::(checkChildren (otherChildren, toParentStr)))
   3.260 +		else (trace "\nNo child output";
   3.261 +		      childProc::(checkChildren (otherChildren, toParentStr)))
   3.262  	       end
   3.263  
   3.264  	
   3.265 @@ -400,15 +344,14 @@
   3.266  (*** add subgoal id num to this *)
   3.267  	fun execCmds  [] procList = procList
   3.268  	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   3.269 -	      let val _ = File.write (File.tmp_path (Path.basic "exec_child"))  
   3.270 +	      let val _ = trace 
   3.271  	                    (space_implode "\n" 
   3.272 -	                      (["About to execute command for goal:",
   3.273 +	                      (["\nAbout to execute command for goal:",
   3.274  	                        goalstring, proverCmd] @ settings @
   3.275  	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   3.276  	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   3.277  		       (Unix.execute(proverCmd, (settings@[file])))
   3.278  		  val (instr, outstr) = Unix.streamsOf childhandle
   3.279 -		  
   3.280  		  val newProcList = (CMDPROC{
   3.281  				       prover = prover,
   3.282  				       cmd = file,
   3.283 @@ -417,12 +360,9 @@
   3.284  				       instr = instr,
   3.285  				       outstr = outstr }) :: procList
   3.286       
   3.287 -		  val _ = File.append (File.tmp_path (Path.basic "exec_child")) 
   3.288 -			    ("\nFinished at " ^
   3.289 -			     Date.toString(Date.fromTimeLocal(Time.now())))
   3.290 -	      in
   3.291 -		execCmds cmds newProcList
   3.292 -	      end
   3.293 +		  val _ = trace ("\nFinished at " ^
   3.294 +			         Date.toString(Date.fromTimeLocal(Time.now())))
   3.295 +	      in execCmds cmds newProcList end
   3.296  
   3.297  
   3.298       (****************************************)                  
   3.299 @@ -446,17 +386,16 @@
   3.300  
   3.301  	 fun keepWatching (procList) = 
   3.302  	   let fun loop procList =  
   3.303 -		let val _ = File.append (File.tmp_path trace_path) 
   3.304 -			       ("\nCalling pollParentInput: " ^ 
   3.305 -			        Int.toString (!iterations_left));
   3.306 +		let val _ = trace ("\nCalling pollParentInput: " ^ 
   3.307 +			           Int.toString (!iterations_left));
   3.308  		    val cmdsFromIsa = pollParentInput 
   3.309  		                       (fromParentIOD, fromParentStr, toParentStr)
   3.310  		in 
   3.311 +		   OS.Process.sleep (Time.fromMilliseconds 100);
   3.312  		   iterations_left := !iterations_left - 1;
   3.313  		   if !iterations_left <= 0 
   3.314 -		   then (*Sadly, this code fails to terminate the watcher!*)
   3.315 -		    (File.append (File.tmp_path trace_path) 
   3.316 -			         "\nTimeout: Killing proof processes";
   3.317 +		   then 
   3.318 +		    (trace "\nTimeout: Killing proof processes";
   3.319  	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   3.320  		     TextIO.flushOut toParentStr;
   3.321  		     killChildren (map cmdchildHandle procList);
   3.322 @@ -476,13 +415,11 @@
   3.323  			 let 
   3.324  			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   3.325  			   val _ = Posix.ProcEnv.getppid()
   3.326 -			   val _ = File.append (File.tmp_path trace_path)
   3.327 -			      "\nJust execed a child"
   3.328 +			   val _ = trace "\nJust execed a child"
   3.329  			   val newProcList' = checkChildren (newProcList, toParentStr) 
   3.330  			 in
   3.331 -			   File.append (File.tmp_path trace_path) 
   3.332 -			       ("\nOff to keep watching: " ^ 
   3.333 -			        Int.toString (!iterations_left));
   3.334 +			   trace ("\nOff to keep watching: " ^ 
   3.335 +			          Int.toString (!iterations_left));
   3.336  			   loop newProcList'
   3.337  			 end
   3.338  		       else  (* Execute remotely              *)
   3.339 @@ -497,9 +434,8 @@
   3.340  		   else (* No new input from Isabelle *)
   3.341  		     let val newProcList = checkChildren (procList, toParentStr)
   3.342  		     in
   3.343 -		       File.append (File.tmp_path trace_path) 
   3.344 -			       ("\nNo new input, still watching: " ^ 
   3.345 -			        Int.toString (!iterations_left));
   3.346 +		       trace ("\nNo new input, still watching: " ^ 
   3.347 +			      Int.toString (!iterations_left));
   3.348  		       loop newProcList
   3.349  		     end
   3.350  		 end
   3.351 @@ -583,9 +519,8 @@
   3.352  	  (goals_being_watched := !goals_being_watched - 1;
   3.353  	   if !goals_being_watched = 0
   3.354  	   then 
   3.355 -	     (File.append (File.tmp_path (Path.basic "reap_found"))
   3.356 -	       ("Reaping a watcher, childpid = "^
   3.357 -		LargeWord.toString (Posix.Process.pidToWord childpid)^"\n");
   3.358 +	     (trace ("\nReaping a watcher, childpid = "^
   3.359 +		     LargeWord.toString (Posix.Process.pidToWord childpid));
   3.360  	      killWatcher childpid; reapWatcher (childpid,childin, childout))
   3.361  	    else ())
   3.362       val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
   3.363 @@ -597,24 +532,23 @@
   3.364  		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
   3.365         in 
   3.366  	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
   3.367 -	 then (tracing (Recon_Transfer.apply_res_thm outcome goalstring);
   3.368 +	 then (priority (Recon_Transfer.apply_res_thm outcome goalstring);
   3.369  	       decr_watched())
   3.370  	 else if String.isPrefix "Invalid" outcome
   3.371 -	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "is not provable");
   3.372 +	 then (priority (goalstring ^ "is not provable");
   3.373  	       decr_watched())
   3.374  	 else if String.isPrefix "Failure" outcome
   3.375 -	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "proof attempt failed");
   3.376 +	 then (priority (goalstring ^ "proof attempt failed");
   3.377  	       decr_watched()) 
   3.378  	(* print out a list of rules used from clasimpset*)
   3.379  	 else if String.isPrefix "Success" outcome
   3.380 -	 then (tracing (goalstring^outcome);
   3.381 +	 then (priority (goalstring^outcome);
   3.382  	       decr_watched())
   3.383  	  (* if proof translation failed *)
   3.384  	 else if String.isPrefix "Translation failed" outcome
   3.385 -	 then (tracing (goalstring ^ Recon_Transfer.restore_linebreaks outcome);
   3.386 +	 then (priority (goalstring ^ outcome);
   3.387  	       decr_watched())
   3.388 -	 else  
   3.389 -	      (tracing "System error in proof handler";
   3.390 +	 else (priority "System error in proof handler";
   3.391  	       decr_watched())
   3.392         end
   3.393   in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
     4.1 --- a/src/HOL/Tools/res_atp.ML	Wed Sep 28 11:15:33 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Sep 28 11:16:27 2005 +0200
     4.3 @@ -12,6 +12,7 @@
     4.4    val destdir: string ref
     4.5    val hook_count: int ref
     4.6    val problem_name: string ref
     4.7 +  val time_limit: int ref
     4.8  end;
     4.9  
    4.10  structure ResAtp: RES_ATP =
    4.11 @@ -19,11 +20,11 @@
    4.12  
    4.13  val call_atp = ref false;
    4.14  val hook_count = ref 0;
    4.15 +val time_limit = ref 60;
    4.16  
    4.17  val prover = ref "E";   (* use E as the default prover *)
    4.18  val custom_spass =   (*specialized options for SPASS*)
    4.19 -      ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
    4.20 -           "-DocProof","-TimeLimit=60"];
    4.21 +      ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    4.22  
    4.23  val destdir = ref "";   (*Empty means write files to /tmp*)
    4.24  val problem_name = ref "prob";
    4.25 @@ -104,6 +105,7 @@
    4.26              val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
    4.27  
    4.28              val probfile = prob_pathname() ^ "_" ^ Int.toString n
    4.29 +            val time = Int.toString (!time_limit)
    4.30              val _ = debug ("problem file in watcher_call_provers is " ^ probfile)
    4.31            in
    4.32              (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
    4.33 @@ -114,8 +116,9 @@
    4.34  		      if !AtpCommunication.reconstruct 
    4.35  		          (*Proof reconstruction works for only a limited set of 
    4.36  		            inference rules*)
    4.37 -                      then "-" ^ space_implode "%-" (!custom_spass)
    4.38 -                      else "-DocProof%-TimeLimit=60%-SOS%-FullRed=0" (*Auto mode*)
    4.39 +                      then space_implode "%" (!custom_spass) ^
    4.40 +                           "%-DocProof%-TimeLimit=" ^ time
    4.41 +                      else "-DocProof%-SOS%-FullRed=0%-TimeLimit=" ^ time (*Auto mode*)
    4.42                    val _ = debug ("SPASS option string is " ^ optionline)
    4.43                    val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    4.44                      (*We've checked that SPASS is there for ATP/spassshell to run.*)
    4.45 @@ -129,7 +132,7 @@
    4.46  	    then 
    4.47                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vampire"
    4.48                in
    4.49 -                ([("vampire", goalstring, vampire, "-t 60%-m 100000", probfile)] @
    4.50 +                ([("vampire", goalstring, vampire, "-m 100000%-t " ^ time, probfile)] @
    4.51                   (make_atp_list xs (n+1)))       (*BEWARE! spaces in options!*)
    4.52                end
    4.53        	     else if !prover = "E"
    4.54 @@ -137,7 +140,7 @@
    4.55  	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
    4.56  	       in
    4.57  		  ([("E", goalstring, Eprover, 
    4.58 -		     "--tptp-in%-l5%-xAuto%-tAuto%--soft-cpu-limit=60",
    4.59 +		     "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time,
    4.60  		     probfile)] @
    4.61  		   (make_atp_list xs (n+1)))
    4.62  	       end
    4.63 @@ -237,7 +240,7 @@
    4.64      hook_count := !hook_count +1;
    4.65      debug ("in hook for time: " ^(Int.toString (!hook_count)) );
    4.66      ResClause.init thy;
    4.67 -    if !destdir = "" then isar_atp (ctxt, goal)
    4.68 +    if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
    4.69      else isar_atp_writeonly (ctxt, goal)
    4.70    end);
    4.71