src/HOL/Tools/ATP/watcher.ML
changeset 17306 5cde710a8a23
parent 17305 6cef3aedd661
child 17315 5bf0e0aacc24
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Wed Sep 07 09:54:31 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Sep 07 18:14:26 2005 +0200
     1.3 @@ -328,76 +328,63 @@
     1.4  	   val sign = sign_of_thm thm
     1.5  	   val prems = prems_of thm
     1.6  	   val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
     1.7 -	   val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
     1.8 -	  (* tracing *)
     1.9 -	 (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
    1.10 -	   val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
    1.11 -	   val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
    1.12 -	   val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
    1.13 -	   val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
    1.14 -	   val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
    1.15 -		    *)
    1.16 -	   (*val goalstr = string_of_thm (the_goal)
    1.17 -	    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher")));  
    1.18 -	   val _ = TextIO.output (outfile,goalstr )
    1.19 -	   val _ =  TextIO.closeOut outfile*)
    1.20 +	   val _ = debug ("subgoals forked to startWatcher: "^prems_string);
    1.21  	   fun killChildren [] = ()
    1.22 -	|      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
    1.23 +	|      killChildren  (child_handle::children) =
    1.24 +	         (killChild child_handle; killChildren children)
    1.25  
    1.26  	 (*************************************************************)
    1.27  	 (* take an instream and poll its underlying reader for input *)
    1.28  	 (*************************************************************)
    1.29  
    1.30  	 fun pollParentInput () = 
    1.31 -	    let val pd = OS.IO.pollDesc (fromParentIOD)
    1.32 -	    in 
    1.33 -	      if (isSome pd ) then 
    1.34 -		  let val pd' = OS.IO.pollIn (valOf pd)
    1.35 -		      val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
    1.36 -		      val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
    1.37 -			("In parent_poll\n")	
    1.38 -		  in
    1.39 -		     if null pdl 
    1.40 -		     then
    1.41 -			NONE
    1.42 -		     else if (OS.IO.isIn (hd pdl)) 
    1.43 -			  then SOME (getCmds (toParentStr, fromParentStr, []))
    1.44 -			  else NONE
    1.45 -		  end
    1.46 -		else NONE
    1.47 -	    end
    1.48 +	   let val pd = OS.IO.pollDesc (fromParentIOD)
    1.49 +	   in 
    1.50 +	     if isSome pd then 
    1.51 +		 let val pd' = OS.IO.pollIn (valOf pd)
    1.52 +		     val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
    1.53 +		     val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
    1.54 +		       ("In parent_poll\n")	
    1.55 +		 in
    1.56 +		    if null pdl 
    1.57 +		    then
    1.58 +		       NONE
    1.59 +		    else if (OS.IO.isIn (hd pdl)) 
    1.60 +			 then SOME (getCmds (toParentStr, fromParentStr, []))
    1.61 +			 else NONE
    1.62 +		 end
    1.63 +	       else NONE
    1.64 +	   end
    1.65  		 
    1.66  	  fun pollChildInput (fromStr) = 
    1.67 -	    let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
    1.68 -			  ("In child_poll\n")
    1.69 -		val iod = getInIoDesc fromStr
    1.70 -	    in 
    1.71 -	      if isSome iod 
    1.72 -	      then 
    1.73 -		let val pd = OS.IO.pollDesc (valOf iod)
    1.74 -		in 
    1.75 -		if (isSome pd ) then 
    1.76 -		    let val pd' = OS.IO.pollIn (valOf pd)
    1.77 -			val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
    1.78 -		    in
    1.79 -		       if null pdl 
    1.80 -		       then
    1.81 -			 ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
    1.82 -			  ("Null pdl \n");NONE)
    1.83 -		       else if (OS.IO.isIn (hd pdl)) 
    1.84 -			    then
    1.85 -				(let val inval =  (TextIO.inputLine fromStr)
    1.86 -				     val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
    1.87 -				 in
    1.88 -				       SOME inval
    1.89 -				 end)
    1.90 -			    else
    1.91 -				  ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
    1.92 -			  ("Null pdl \n");NONE)
    1.93 -		    end
    1.94 -		  else  NONE
    1.95 -		  end
    1.96 -	      else NONE
    1.97 +	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
    1.98 +			 ("In child_poll\n")
    1.99 +	       val iod = getInIoDesc fromStr
   1.100 +	   in 
   1.101 +	     if isSome iod 
   1.102 +	     then 
   1.103 +	       let val pd = OS.IO.pollDesc (valOf iod)
   1.104 +	       in 
   1.105 +	       if isSome pd then 
   1.106 +		   let val pd' = OS.IO.pollIn (valOf pd)
   1.107 +		       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   1.108 +		   in
   1.109 +		      if null pdl 
   1.110 +		      then
   1.111 +			(File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl\n"; 
   1.112 +			 NONE)
   1.113 +		      else if OS.IO.isIn (hd pdl)
   1.114 +		      then
   1.115 +			   let val inval =  (TextIO.inputLine fromStr)
   1.116 +			       val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
   1.117 +			   in SOME inval end
   1.118 +		      else
   1.119 +                        (File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl \n";
   1.120 +                         NONE)
   1.121 +		   end
   1.122 +		 else NONE
   1.123 +		 end
   1.124 +	     else NONE
   1.125  	end
   1.126  
   1.127  
   1.128 @@ -434,37 +421,37 @@
   1.129  		   val sign = sign_of_thm thm
   1.130  		   val prems = prems_of thm
   1.131  		   val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.132 -		   val _ = warning("subgoals forked to checkChildren: "^prems_string)
   1.133 +		   val _ = debug("subgoals forked to checkChildren: "^prems_string)
   1.134  		   val goalstring = cmdGoal childProc							
   1.135  		   val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
   1.136  			      (prover^thmstring^goalstring^childCmd^"\n")
   1.137  	       in 
   1.138 -		 if (isSome childIncoming) 
   1.139 +		 if isSome childIncoming
   1.140  		 then 
   1.141 -		     (* check here for prover label on child*)
   1.142 -		     let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) 
   1.143 -				("subgoals forked to checkChildren:"^
   1.144 -				prems_string^prover^thmstring^goalstring^childCmd) 
   1.145 -			 val childDone = (case prover of
   1.146 -			     "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )     
   1.147 -                              | "E" => (EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )              
   1.148 -			    |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   1.149 -		      in
   1.150 -		       if childDone      (**********************************************)
   1.151 -		       then (* child has found a proof and transferred it *)
   1.152 -			  (* Remove this child and go on to check others*)
   1.153 -			  (**********************************************)
   1.154 -			  (Unix.reap child_handle;
   1.155 -			   checkChildren(otherChildren, toParentStr))
   1.156 -		       else 
   1.157 -			  (**********************************************)
   1.158 -			  (* Keep this child and go on to check others  *)
   1.159 -			  (**********************************************)
   1.160 -			 (childProc::(checkChildren (otherChildren, toParentStr)))
   1.161 -		    end
   1.162 -		  else
   1.163 -		    (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   1.164 -		     childProc::(checkChildren (otherChildren, toParentStr)))
   1.165 +		   (* check here for prover label on child*)
   1.166 +		   let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) 
   1.167 +			      ("subgoals forked to checkChildren:"^
   1.168 +			      prems_string^prover^thmstring^goalstring^childCmd) 
   1.169 +		       val childDone = (case prover of
   1.170 +			   "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  
   1.171 +			    | "E" => EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
   1.172 +			  |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  )
   1.173 +		    in
   1.174 +		     if childDone      (**********************************************)
   1.175 +		     then (* child has found a proof and transferred it *)
   1.176 +			(* Remove this child and go on to check others*)
   1.177 +			(**********************************************)
   1.178 +			(Unix.reap child_handle;
   1.179 +			 checkChildren(otherChildren, toParentStr))
   1.180 +		     else 
   1.181 +			(**********************************************)
   1.182 +			(* Keep this child and go on to check others  *)
   1.183 +			(**********************************************)
   1.184 +		       (childProc::(checkChildren (otherChildren, toParentStr)))
   1.185 +		  end
   1.186 +		else
   1.187 +		  (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   1.188 +		   childProc::(checkChildren (otherChildren, toParentStr)))
   1.189  	       end
   1.190  
   1.191  	
   1.192 @@ -480,7 +467,7 @@
   1.193  	fun execCmds  [] procList = procList
   1.194  	|   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =             let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child"))  ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   1.195  	  in 
   1.196 -	    if (prover = "spass") 
   1.197 +	    if prover = "spass"
   1.198  	    then 
   1.199  	      let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   1.200  		       (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   1.201 @@ -495,7 +482,8 @@
   1.202  				       outstr = outstr })::procList))
   1.203  		   val _ = File.append (File.tmp_path (Path.basic "exec_child"))  
   1.204  			("\nexecuting command for goal:\n"^
   1.205 -			 goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   1.206 +			 goalstring^proverCmd^(concat settings)^file^
   1.207 +			 " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   1.208  	      in
   1.209  		 Posix.Process.sleep (Time.fromSeconds 1);
   1.210  		 execCmds cmds newProcList
   1.211 @@ -546,31 +534,33 @@
   1.212       (**********************************************)                  
   1.213       (* Watcher Loop                               *)
   1.214       (**********************************************)
   1.215 +         val iterations_left = ref 1000;  (*200 seconds, 5 iterations per sec*)
   1.216  
   1.217  	 fun keepWatching (toParentStr, fromParentStr,procList) = 
   1.218  	   let fun loop (procList) =  
   1.219  		let val _ = Posix.Process.sleep (Time.fromMilliseconds 200)
   1.220  		    val cmdsFromIsa = pollParentInput ()
   1.221 -		    fun killchildHandler (n:int)  = 
   1.222 -			  (TextIO.output(toParentStr, "Killing child proof processes!\n");
   1.223 +		    fun killchildHandler ()  = 
   1.224 +			  (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   1.225  			   TextIO.flushOut toParentStr;
   1.226  			   killChildren (map (cmdchildHandle) procList);
   1.227  			   ())
   1.228  		in 
   1.229  		   (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   1.230 -								      (**********************************)
   1.231 -		   if (isSome cmdsFromIsa) 
   1.232 +		   iterations_left := !iterations_left - 1;
   1.233 +		   if !iterations_left = 0 then killchildHandler ()
   1.234 +		   else if isSome cmdsFromIsa
   1.235  		   then (*  deal with input from Isabelle *)
   1.236 -		     if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   1.237 +		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
   1.238  		     then 
   1.239  		       let val child_handles = map cmdchildHandle procList 
   1.240  		       in
   1.241  			  killChildren child_handles;
   1.242  			  (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)    
   1.243 -			  loop ([])
   1.244 +			  loop []
   1.245  		       end
   1.246  		     else
   1.247 -		       if ((length procList)<10)    (********************)
   1.248 +		       if length procList < 5     (********************)
   1.249  		       then                        (* Execute locally  *)
   1.250  			 let 
   1.251  			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.252 @@ -578,10 +568,10 @@
   1.253  			      val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
   1.254  			   val newProcList' =checkChildren (newProcList, toParentStr) 
   1.255  
   1.256 -			   val _ = warning("off to keep watching...")
   1.257 +			   val _ = debug("off to keep watching...")
   1.258  			  val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
   1.259  			 in
   1.260 -			   loop (newProcList') 
   1.261 +			   loop newProcList'
   1.262  			 end
   1.263  		       else  (* Execute remotely              *)
   1.264  			     (* (actually not remote for now )*)
   1.265 @@ -590,17 +580,17 @@
   1.266  			   val parentID = Posix.ProcEnv.getppid()
   1.267  			   val newProcList' =checkChildren (newProcList, toParentStr) 
   1.268  			 in
   1.269 -			   loop (newProcList') 
   1.270 +			   loop newProcList'
   1.271  			 end
   1.272  		   else (* No new input from Isabelle *)
   1.273  		     let val newProcList = checkChildren ((procList), toParentStr)
   1.274  		     in
   1.275  		      (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
   1.276 -		       loop (newProcList)
   1.277 +		       loop newProcList
   1.278  		     end
   1.279  		 end
   1.280  	   in  
   1.281 -	       loop (procList)
   1.282 +	       loop procList
   1.283  	   end
   1.284  	   
   1.285  
   1.286 @@ -678,7 +668,8 @@
   1.287  	  status
   1.288    end
   1.289  
   1.290 -fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) =
   1.291 +
   1.292 +fun createWatcher (thm,clause_arr, num_of_clauses) =
   1.293   let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   1.294       val streams = snd mychild
   1.295       val childin = fst streams
   1.296 @@ -687,34 +678,33 @@
   1.297       val sign = sign_of_thm thm
   1.298       val prems = prems_of thm
   1.299       val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.300 -     val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   1.301 +     val _ = debug ("subgoals forked to createWatcher: "^prems_string);
   1.302 +(*FIXME: do we need an E proofHandler??*)
   1.303       fun vampire_proofHandler (n) =
   1.304  	(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.305  	 VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))               
   1.306       fun spass_proofHandler (n) = (
   1.307 -       let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
   1.308 -	   val _ = TextIO.output (outfile, ("In signal handler now\n"))
   1.309 -	   val _ =  TextIO.closeOut outfile
   1.310 +       let val _ = File.append (File.tmp_path (Path.basic "spass_signal_in"))
   1.311 +                               "Starting SPASS signal handler\n"
   1.312  	   val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
   1.313 -	   val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
   1.314 -   
   1.315 -	   val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   1.316 -	   val _ =  TextIO.closeOut outfile
   1.317 +	   val _ = File.append (File.tmp_path (Path.basic "spass_signal_out"))
   1.318 +		       ("In SPASS signal handler "^reconstr^thmstring^goalstring^
   1.319 +		       "goals_being_watched: "^ string_of_int (!goals_being_watched))
   1.320         in (* if a proof has been found and sent back as a reconstruction proof *)
   1.321  	 if substring (reconstr, 0,1) = "["
   1.322  	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.323  	       Recon_Transfer.apply_res_thm reconstr goalstring;
   1.324  	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.325  	       
   1.326 -	       goals_being_watched := ((!goals_being_watched) - 1);
   1.327 +	       goals_being_watched := (!goals_being_watched) - 1;
   1.328         
   1.329 -	       if (!goals_being_watched) = 0
   1.330 +	       if !goals_being_watched = 0
   1.331  	       then 
   1.332 -		  let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found"))
   1.333 -                                   ("Reaping a watcher, goals watched is: "^
   1.334 -                                    (string_of_int (!goals_being_watched))^"\n")
   1.335 +		  let val _ = File.write (File.tmp_path (Path.basic "reap_found"))
   1.336 +                                   ("Reaping a watcher, goals watched now "^
   1.337 +                                    string_of_int (!goals_being_watched)^"\n")
   1.338  		   in
   1.339 -		       killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   1.340 +		       killWatcher childpid; reapWatcher (childpid,childin, childout); ()
   1.341  		   end
   1.342  		else () )
   1.343  	 (* if there's no proof, but a message from Spass *)