src/HOL/Tools/ATP/watcher.ML
changeset 17317 3f12de2e2e6e
parent 17315 5bf0e0aacc24
child 17422 3b237822985d
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Sep 09 12:18:15 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Sep 09 17:47:37 2005 +0200
     1.3 @@ -87,15 +87,12 @@
     1.4  
     1.5  
     1.6  fun reap(pid, instr, outstr) =
     1.7 -        let
     1.8 -		val u = TextIO.closeIn instr;
     1.9 -	        val u = TextIO.closeOut outstr;
    1.10 -	
    1.11 -		val (_, status) =
    1.12 -			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    1.13 -	in
    1.14 -		status
    1.15 -	end
    1.16 +  let val u = TextIO.closeIn instr;
    1.17 +      val u = TextIO.closeOut outstr;
    1.18 +      val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    1.19 +  in
    1.20 +	  status
    1.21 +  end
    1.22  
    1.23  fun fdReader (name : string, fd : Posix.IO.file_desc) =
    1.24  	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    1.25 @@ -106,8 +103,7 @@
    1.26                initBlkMode = true,
    1.27                name = name,  
    1.28                chunkSize=4096,
    1.29 -              fd = fd
    1.30 -            };
    1.31 +              fd = fd};
    1.32  
    1.33  fun openOutFD (name, fd) =
    1.34  	  TextIO.mkOutstream (
    1.35 @@ -125,38 +121,31 @@
    1.36  
    1.37  fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
    1.38  
    1.39 -fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
    1.40 -
    1.41 -fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = (prover,(cmd, (instr,outstr)));
    1.42 +fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
    1.43  
    1.44 -fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = proc_handle;
    1.45 +fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = 
    1.46 +  (prover,(cmd, (instr,outstr)));
    1.47  
    1.48 -fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (prover);
    1.49 -
    1.50 -fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (thmstring);
    1.51 +fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = 
    1.52 +  proc_handle;
    1.53  
    1.54 -fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (goalstring);
    1.55 -
    1.56 -fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
    1.57 +fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  =
    1.58 +  prover;
    1.59  
    1.60 -(********************************************************************************************)
    1.61 -(*  takes a list of arguments and sends them individually to the watcher process by pipe    *)
    1.62 -(********************************************************************************************)
    1.63 +fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = 
    1.64 +  thmstring;
    1.65  
    1.66 -fun outputArgs (toWatcherStr, []) = ()
    1.67 -|   outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); 
    1.68 -                                          TextIO.flushOut toWatcherStr;
    1.69 -                                         outputArgs (toWatcherStr, xs))
    1.70 +fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  =
    1.71 +  goalstring;
    1.72 +
    1.73  
    1.74  (********************************************************************************)
    1.75  (*    gets individual args from instream and concatenates them into a list      *)
    1.76  (********************************************************************************)
    1.77  
    1.78 -fun getArgs (fromParentStr, toParentStr,ys) =  let 
    1.79 -                                       val thisLine = TextIO.input fromParentStr
    1.80 -                                    in
    1.81 -                                        ((ys@[thisLine]))
    1.82 -                                    end
    1.83 +fun getArgs (fromParentStr, toParentStr, ys) =  
    1.84 +  let val thisLine = TextIO.input fromParentStr
    1.85 +  in ys@[thisLine] end
    1.86  
    1.87                              
    1.88  (********************************************************************************)
    1.89 @@ -164,7 +153,7 @@
    1.90  (********************************************************************************)
    1.91                      
    1.92  fun callResProver (toWatcherStr,  arg) = 
    1.93 -      (sendOutput (toWatcherStr, arg^"\n"); 
    1.94 +      (TextIO.output (toWatcherStr, arg^"\n"); 
    1.95         TextIO.flushOut toWatcherStr)
    1.96  
    1.97  (*****************************************************************************************)
    1.98 @@ -175,14 +164,14 @@
    1.99      
   1.100  (*Uses the $-character to separate items sent to watcher*)
   1.101  fun callResProvers (toWatcherStr,  []) = 
   1.102 -      (sendOutput (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
   1.103 +      (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
   1.104  |   callResProvers (toWatcherStr,
   1.105                      (prover,thmstring,goalstring, proverCmd,settings, 
   1.106                       axfile, hypsfile,probfile)  ::  args) =
   1.107        let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
   1.108                               (prover^thmstring^goalstring^proverCmd^settings^
   1.109                                hypsfile^probfile)
   1.110 -      in sendOutput (toWatcherStr,    
   1.111 +      in TextIO.output (toWatcherStr,    
   1.112              (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^
   1.113               settings^"$"^hypsfile^"$"^probfile^"\n"));
   1.114           goals_being_watched := (!goals_being_watched) + 1;
   1.115 @@ -196,7 +185,7 @@
   1.116  (* Send message to watcher to kill currently running vampires *)
   1.117  (**************************************************************)
   1.118  
   1.119 -fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 
   1.120 +fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n"); 
   1.121                              TextIO.flushOut toWatcherStr)
   1.122  
   1.123  
   1.124 @@ -262,7 +251,7 @@
   1.125  	     TextIO.flushOut toParentStr;
   1.126  	   (("","","","Kill children",[],"")::cmdList)
   1.127  	  )
   1.128 -     else  let val thisCmd = getCmd (thisLine) 
   1.129 +     else  let val thisCmd = getCmd thisLine 
   1.130  	       (*********************************************************)
   1.131  	       (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   1.132  	       (* i.e. put back into tuple format                       *)
   1.133 @@ -270,7 +259,7 @@
   1.134  	   in
   1.135  	     (*TextIO.output (toParentStr, thisCmd); 
   1.136  	       TextIO.flushOut toParentStr;*)
   1.137 -	       getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
   1.138 +	       getCmds (toParentStr, fromParentStr, (thisCmd::cmdList))
   1.139  	   end
   1.140    end
   1.141  	    
   1.142 @@ -302,16 +291,15 @@
   1.143      (** pipes for communication between parent and watcher **)
   1.144      val p1 = Posix.IO.pipe ()
   1.145      val p2 = Posix.IO.pipe ()
   1.146 -    fun closep () = (
   1.147 -	  Posix.IO.close (#outfd p1); 
   1.148 +    fun closep () = 
   1.149 +	 (Posix.IO.close (#outfd p1); 
   1.150  	  Posix.IO.close (#infd p1);
   1.151  	  Posix.IO.close (#outfd p2); 
   1.152 -	  Posix.IO.close (#infd p2)
   1.153 -	)
   1.154 +	  Posix.IO.close (#infd p2))
   1.155      (***********************************************************)
   1.156      (****** fork a watcher process and get it set up and going *)
   1.157      (***********************************************************)
   1.158 -    fun startWatcher (procList) =
   1.159 +    fun startWatcher procList =
   1.160       (case  Posix.Process.fork() (***************************************)
   1.161        of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   1.162  				    (***************************************)
   1.163 @@ -338,7 +326,7 @@
   1.164  	 (*************************************************************)
   1.165  
   1.166  	 fun pollParentInput () = 
   1.167 -	   let val pd = OS.IO.pollDesc (fromParentIOD)
   1.168 +	   let val pd = OS.IO.pollDesc fromParentIOD
   1.169  	   in 
   1.170  	     if isSome pd then 
   1.171  		 let val pd' = OS.IO.pollIn (valOf pd)
   1.172 @@ -356,7 +344,7 @@
   1.173  	       else NONE
   1.174  	   end
   1.175  		 
   1.176 -	  fun pollChildInput (fromStr) = 
   1.177 +	  fun pollChildInput fromStr = 
   1.178  	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
   1.179  			 ("In child_poll\n")
   1.180  	       val iod = getInIoDesc fromStr
   1.181 @@ -465,31 +453,13 @@
   1.182  
   1.183  (*** add subgoal id num to this *)
   1.184  	fun execCmds  [] procList = procList
   1.185 -	|   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.186 -	  in 
   1.187 -	    if prover = "spass"
   1.188 -	    then 
   1.189 -	      let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   1.190 -		       (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   1.191 -		  val (instr, outstr) = Unix.streamsOf childhandle
   1.192 -		  val newProcList =    (((CMDPROC{
   1.193 -				       prover = prover,
   1.194 -				       cmd = file,
   1.195 -				       thmstring = thmstring,
   1.196 -				       goalstring = goalstring,
   1.197 -				       proc_handle = childhandle,
   1.198 -				       instr = instr,
   1.199 -				       outstr = outstr })::procList))
   1.200 -		   val _ = File.append (File.tmp_path (Path.basic "exec_child"))  
   1.201 -			("\nexecuting command for goal:\n"^
   1.202 -			 goalstring^proverCmd^(concat settings)^file^
   1.203 -			 " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   1.204 -	      in
   1.205 -		 Posix.Process.sleep (Time.fromSeconds 1);
   1.206 -		 execCmds cmds newProcList
   1.207 -	      end
   1.208 -	    else 
   1.209 -	      let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   1.210 +	|   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =
   1.211 +	      let val _ = File.write (File.tmp_path (Path.basic "exec_child"))  
   1.212 +	                    (space_implode "\n" 
   1.213 +	                      (["About to execute command for goal:",
   1.214 +	                        goalstring, proverCmd] @ settings @
   1.215 +	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   1.216 +	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   1.217  		       (Unix.execute(proverCmd, (settings@[file])))
   1.218  		  val (instr, outstr) = Unix.streamsOf childhandle
   1.219  		  
   1.220 @@ -503,20 +473,18 @@
   1.221  				       outstr = outstr }) :: procList
   1.222       
   1.223  		  val _ = File.append (File.tmp_path (Path.basic "exec_child")) 
   1.224 -			    ("executing command for goal:\n"^
   1.225 -			     goalstring^proverCmd^(concat settings)^file^
   1.226 -			     " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   1.227 +			    ("\nFinished at " ^
   1.228 +			     Date.toString(Date.fromTimeLocal(Time.now())))
   1.229  	      in
   1.230  		Posix.Process.sleep (Time.fromSeconds 1); 
   1.231  		execCmds cmds newProcList
   1.232  	      end
   1.233 -	   end
   1.234  
   1.235  
   1.236       (****************************************)                  
   1.237       (* call resolution processes remotely   *)
   1.238       (* settings should be a list of strings *)
   1.239 -     (* e.g. ["-t 300", "-m 100000"]         *)
   1.240 +     (* e.g. ["-t300", "-m100000"]         *)
   1.241       (****************************************)
   1.242  
   1.243        (*  fun execRemoteCmds  [] procList = procList
   1.244 @@ -527,23 +495,19 @@
   1.245  				      end
   1.246  *)
   1.247  
   1.248 -	fun printList (outStr, []) = ()
   1.249 -	|   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   1.250 -
   1.251 -
   1.252       (**********************************************)                  
   1.253       (* Watcher Loop                               *)
   1.254       (**********************************************)
   1.255           val iterations_left = ref 1000;  (*200 seconds, 5 iterations per sec*)
   1.256  
   1.257  	 fun keepWatching (toParentStr, fromParentStr,procList) = 
   1.258 -	   let fun loop (procList) =  
   1.259 +	   let fun loop procList =  
   1.260  		let val _ = Posix.Process.sleep (Time.fromMilliseconds 200)
   1.261  		    val cmdsFromIsa = pollParentInput ()
   1.262  		    fun killchildHandler ()  = 
   1.263  			  (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   1.264  			   TextIO.flushOut toParentStr;
   1.265 -			   killChildren (map (cmdchildHandle) procList);
   1.266 +			   killChildren (map cmdchildHandle procList);
   1.267  			   ())
   1.268  		in 
   1.269  		   (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   1.270 @@ -583,7 +547,7 @@
   1.271  			   loop newProcList'
   1.272  			 end
   1.273  		   else (* No new input from Isabelle *)
   1.274 -		     let val newProcList = checkChildren ((procList), toParentStr)
   1.275 +		     let val newProcList = checkChildren (procList, toParentStr)
   1.276  		     in
   1.277  		      (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
   1.278  		       loop newProcList
   1.279 @@ -625,7 +589,7 @@
   1.280      (*******************************)
   1.281  
   1.282      val procList = []
   1.283 -    val pid = startWatcher (procList)
   1.284 +    val pid = startWatcher procList
   1.285      (**************************************************)
   1.286      (* communication streams to watcher               *)
   1.287      (**************************************************)
   1.288 @@ -680,10 +644,10 @@
   1.289       val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.290       val _ = debug ("subgoals forked to createWatcher: "^prems_string);
   1.291  (*FIXME: do we need an E proofHandler??*)
   1.292 -     fun vampire_proofHandler (n) =
   1.293 +     fun vampire_proofHandler n =
   1.294  	(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.295  	 VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))               
   1.296 -     fun spass_proofHandler (n) = (
   1.297 +     fun spass_proofHandler n = (
   1.298         let val _ = File.append (File.tmp_path (Path.basic "spass_signal_in"))
   1.299                                 "Starting SPASS signal handler\n"
   1.300  	   val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
   1.301 @@ -717,7 +681,7 @@
   1.302  	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.303  	              ("Reaping a watcher, goals watched is: " ^
   1.304  	                 (string_of_int (!goals_being_watched))^"\n");
   1.305 -	             killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
   1.306 +	             killWatcher childpid; reapWatcher (childpid,childin, childout); ())
   1.307  		else () ) 
   1.308  	(* print out a list of rules used from clasimpset*)
   1.309  	 else if substring (reconstr, 0,5) = "Rules"
   1.310 @@ -729,7 +693,7 @@
   1.311  	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.312  	              ("Reaping a watcher, goals watched is: " ^
   1.313  	                 (string_of_int (!goals_being_watched))^"\n");
   1.314 -	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   1.315 +	             killWatcher childpid;  reapWatcher (childpid,childin, childout);()
   1.316  		     )
   1.317  	       else () )
   1.318  	  (* if proof translation failed *)
   1.319 @@ -742,7 +706,7 @@
   1.320  	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.321  	              ("Reaping a watcher, goals watched is: " ^
   1.322  	                 (string_of_int (!goals_being_watched))^"\n");
   1.323 -	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   1.324 +	             killWatcher childpid;  reapWatcher (childpid,childin, childout);()
   1.325  		     )
   1.326  	       else () )
   1.327  
   1.328 @@ -755,7 +719,7 @@
   1.329  	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.330  	              ("Reaping a watcher, goals watched is: " ^
   1.331  	                 (string_of_int (!goals_being_watched))^"\n");
   1.332 -	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   1.333 +	             killWatcher childpid;  reapWatcher (childpid,childin, childout);()
   1.334  		     )
   1.335  	       else () )
   1.336  
   1.337 @@ -768,7 +732,7 @@
   1.338  	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.339  		     ("Reaping a watcher, goals watched is: " ^
   1.340  			(string_of_int (!goals_being_watched))^"\n");
   1.341 -		    killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   1.342 +		    killWatcher childpid;  reapWatcher (childpid,childin, childout);()
   1.343  		    )
   1.344  	       else () )
   1.345         end)