src/HOL/Tools/ATP/watcher.ML
changeset 16061 8a139c1557bf
parent 16039 dfe264950511
child 16089 9169bdf930f8
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue May 24 07:43:38 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Tue May 24 10:23:24 2005 +0200
     1.3 @@ -164,44 +164,45 @@
     1.4  fun callResProvers (toWatcherStr,  []) = (sendOutput (toWatcherStr, "End of calls\n"); 
     1.5                                       TextIO.flushOut toWatcherStr)
     1.6  |   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) =
     1.7 -                                                     let val dfg_dir = File.tmp_path (Path.basic "dfg"); 
     1.8 -                                                        (*** need to check here if the directory exists and, if not, create it***)
     1.9 -                                                         val  outfile = TextIO.openAppend(File.sysify_path
    1.10 -                                                                               (File.tmp_path (Path.basic"thmstring_in_watcher")));                                                                         val _ = TextIO.output (outfile, 
    1.11 -                                                                       (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
    1.12 -                                                         val _ =  TextIO.closeOut outfile
    1.13 -                                                        (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    1.14 -							val probID = last(explode probfile)
    1.15 -                                                         val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    1.16 -                                                         (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    1.17 -                                                         (*** hyps/local axioms just now                                                ***)
    1.18 -                                                         val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
    1.19 -                                                         val dfg_create =if File.exists dfg_dir 
    1.20 -                                                                         then
    1.21 -                                                                             ((warning("dfg dir exists"));())
    1.22 -                                                                         else
    1.23 -                                                                               File.mkdir dfg_dir; 
    1.24 -                                                         
    1.25 -                                                         val dfg_path = File.sysify_path dfg_dir;
    1.26 -                                                         val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X",   ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
    1.27 -                                                       (*val _ = Posix.Process.wait ()*)
    1.28 -                                                       (*val _ =Unix.reap exec_tptp2x*)
    1.29 -                                                         val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
    1.30 -                                       
    1.31 -                                                      in   
    1.32 -                                                         goals_being_watched := (!goals_being_watched) + 1;
    1.33 -                                                         Posix.Process.sleep(Time.fromSeconds 1); 
    1.34 -                     					(warning ("probfile is: "^probfile));
    1.35 -                                                         (warning("dfg file is: "^newfile));
    1.36 -                                                         (warning ("wholefile is: "^(File.sysify_path wholefile)));
    1.37 -                                                        sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
    1.38 -(*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
    1.39 -                                                         TextIO.flushOut toWatcherStr;
    1.40 -                                                         Unix.reap exec_tptp2x; 
    1.41 -                                                         
    1.42 -                                                         callResProvers (toWatcherStr,args)
    1.43 -                                           
    1.44 -                                                     end
    1.45 +      let val dfg_dir = File.tmp_path (Path.basic "dfg"); 
    1.46 +	 (*** need to check here if the directory exists and, if not, create it***)
    1.47 +	  val  outfile = TextIO.openAppend(File.sysify_path
    1.48 +				(File.tmp_path (Path.basic"thmstring_in_watcher")));                                                                         
    1.49 +	  val _ = TextIO.output (outfile, 
    1.50 +			(thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
    1.51 +	  val _ =  TextIO.closeOut outfile
    1.52 +	 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    1.53 +	 val probID = ReconOrderClauses.last(explode probfile)
    1.54 +	  val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    1.55 +	  (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    1.56 +	  (*** hyps/local axioms just now                                                ***)
    1.57 +	  val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
    1.58 +	  val dfg_create =if File.exists dfg_dir 
    1.59 +			  then
    1.60 +			      ((warning("dfg dir exists"));())
    1.61 +			  else
    1.62 +				File.mkdir dfg_dir; 
    1.63 +	  
    1.64 +	  val dfg_path = File.sysify_path dfg_dir;
    1.65 +	  val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X",   ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
    1.66 +	(*val _ = Posix.Process.wait ()*)
    1.67 +	(*val _ =Unix.reap exec_tptp2x*)
    1.68 +	  val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
    1.69 + 
    1.70 +       in   
    1.71 +	  goals_being_watched := (!goals_being_watched) + 1;
    1.72 +	  Posix.Process.sleep(Time.fromSeconds 1); 
    1.73 +	 (warning ("probfile is: "^probfile));
    1.74 +	  (warning("dfg file is: "^newfile));
    1.75 +	  (warning ("wholefile is: "^(File.sysify_path wholefile)));
    1.76 +	 sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
    1.77 + (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
    1.78 +	  TextIO.flushOut toWatcherStr;
    1.79 +	  Unix.reap exec_tptp2x; 
    1.80 +	  
    1.81 +	  callResProvers (toWatcherStr,args)
    1.82 + 
    1.83 +      end
    1.84  (*
    1.85  fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
    1.86                                       
    1.87 @@ -327,374 +328,375 @@
    1.88  
    1.89  
    1.90  
    1.91 -fun setupWatcher (thm,clause_arr, num_of_clauses) = let
    1.92 -          (** pipes for communication between parent and watcher **)
    1.93 -          val p1 = Posix.IO.pipe ()
    1.94 -          val p2 = Posix.IO.pipe ()
    1.95 -	  fun closep () = (
    1.96 -                Posix.IO.close (#outfd p1); 
    1.97 -                Posix.IO.close (#infd p1);
    1.98 -                Posix.IO.close (#outfd p2); 
    1.99 -                Posix.IO.close (#infd p2)
   1.100 -              )
   1.101 -          (***********************************************************)
   1.102 -          (****** fork a watcher process and get it set up and going *)
   1.103 -          (***********************************************************)
   1.104 -          fun startWatcher (procList) =
   1.105 -                   (case  Posix.Process.fork() (***************************************)
   1.106 -		 of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   1.107 -                                               (***************************************)
   1.108 - 
   1.109 -                                                 (*************************)
   1.110 -                  | NONE => let                  (* child - i.e. watcher  *)
   1.111 -		      val oldchildin = #infd p1  (*************************)
   1.112 -		      val fromParent = Posix.FileSys.wordToFD 0w0
   1.113 -		      val oldchildout = #outfd p2
   1.114 -		      val toParent = Posix.FileSys.wordToFD 0w1
   1.115 -                      val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   1.116 -                      val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   1.117 -                      val toParentStr = openOutFD ("_exec_out_parent", toParent)
   1.118 -                      val sign = sign_of_thm thm
   1.119 -                      val prems = prems_of thm
   1.120 -                      val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.121 -                      val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
   1.122 -                     (* tracing *)
   1.123 -		    (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
   1.124 -                      val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
   1.125 -                      val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
   1.126 -                      val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
   1.127 -                      val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
   1.128 -                      val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
   1.129 -                               *)
   1.130 -                      (*val goalstr = string_of_thm (the_goal)
   1.131 -                       val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));  
   1.132 -                      val _ = TextIO.output (outfile,goalstr )
   1.133 -                      val _ =  TextIO.closeOut outfile*)
   1.134 -                      fun killChildren [] = ()
   1.135 -                   |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
   1.136 +fun setupWatcher (thm,clause_arr, num_of_clauses) = 
   1.137 +  let
   1.138 +    (** pipes for communication between parent and watcher **)
   1.139 +    val p1 = Posix.IO.pipe ()
   1.140 +    val p2 = Posix.IO.pipe ()
   1.141 +    fun closep () = (
   1.142 +	  Posix.IO.close (#outfd p1); 
   1.143 +	  Posix.IO.close (#infd p1);
   1.144 +	  Posix.IO.close (#outfd p2); 
   1.145 +	  Posix.IO.close (#infd p2)
   1.146 +	)
   1.147 +    (***********************************************************)
   1.148 +    (****** fork a watcher process and get it set up and going *)
   1.149 +    (***********************************************************)
   1.150 +    fun startWatcher (procList) =
   1.151 +	     (case  Posix.Process.fork() (***************************************)
   1.152 +	   of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   1.153 +					 (***************************************)
   1.154 +
   1.155 +					   (*************************)
   1.156 +	    | NONE => let                  (* child - i.e. watcher  *)
   1.157 +		val oldchildin = #infd p1  (*************************)
   1.158 +		val fromParent = Posix.FileSys.wordToFD 0w0
   1.159 +		val oldchildout = #outfd p2
   1.160 +		val toParent = Posix.FileSys.wordToFD 0w1
   1.161 +		val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   1.162 +		val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   1.163 +		val toParentStr = openOutFD ("_exec_out_parent", toParent)
   1.164 +		val sign = sign_of_thm thm
   1.165 +		val prems = prems_of thm
   1.166 +		val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.167 +		val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
   1.168 +	       (* tracing *)
   1.169 +	      (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
   1.170 +		val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
   1.171 +		val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
   1.172 +		val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
   1.173 +		val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
   1.174 +		val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
   1.175 +			 *)
   1.176 +		(*val goalstr = string_of_thm (the_goal)
   1.177 +		 val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));  
   1.178 +		val _ = TextIO.output (outfile,goalstr )
   1.179 +		val _ =  TextIO.closeOut outfile*)
   1.180 +		fun killChildren [] = ()
   1.181 +	     |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
   1.182  
   1.183 -                     
   1.184 -           
   1.185 -                    (*************************************************************)
   1.186 -                    (* take an instream and poll its underlying reader for input *)
   1.187 -                    (*************************************************************)
   1.188 +	       
   1.189 +     
   1.190 +	      (*************************************************************)
   1.191 +	      (* take an instream and poll its underlying reader for input *)
   1.192 +	      (*************************************************************)
   1.193  
   1.194 -                    fun pollParentInput () = 
   1.195 -                           
   1.196 -                               let val pd = OS.IO.pollDesc (fromParentIOD)
   1.197 -                               in 
   1.198 -                               if (isSome pd ) then 
   1.199 -                                   let val pd' = OS.IO.pollIn (valOf pd)
   1.200 -                                       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
   1.201 -                                   in
   1.202 -                                      if null pdl 
   1.203 -                                      then
   1.204 -                                         NONE
   1.205 -                                      else if (OS.IO.isIn (hd pdl)) 
   1.206 -                                           then
   1.207 -                                              (SOME ( getCmds (toParentStr, fromParentStr, [])))
   1.208 -                                           else
   1.209 -                                               NONE
   1.210 -                                   end
   1.211 -                                 else
   1.212 -                                     NONE
   1.213 -                                 end
   1.214 -                            
   1.215 -                   
   1.216 +	      fun pollParentInput () = 
   1.217 +		     
   1.218 +			 let val pd = OS.IO.pollDesc (fromParentIOD)
   1.219 +			 in 
   1.220 +			 if (isSome pd ) then 
   1.221 +			     let val pd' = OS.IO.pollIn (valOf pd)
   1.222 +				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
   1.223 +			     in
   1.224 +				if null pdl 
   1.225 +				then
   1.226 +				   NONE
   1.227 +				else if (OS.IO.isIn (hd pdl)) 
   1.228 +				     then
   1.229 +					(SOME ( getCmds (toParentStr, fromParentStr, [])))
   1.230 +				     else
   1.231 +					 NONE
   1.232 +			     end
   1.233 +			   else
   1.234 +			       NONE
   1.235 +			   end
   1.236 +		      
   1.237 +	     
   1.238  
   1.239 -                     fun pollChildInput (fromStr) = 
   1.240 -                           let val iod = getInIoDesc fromStr
   1.241 -                           in 
   1.242 -                           if isSome iod 
   1.243 -                           then 
   1.244 -                               let val pd = OS.IO.pollDesc (valOf iod)
   1.245 -                               in 
   1.246 -                               if (isSome pd ) then 
   1.247 -                                   let val pd' = OS.IO.pollIn (valOf pd)
   1.248 -                                       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
   1.249 -                                   in
   1.250 -                                      if null pdl 
   1.251 -                                      then
   1.252 -                                         NONE
   1.253 -                                      else if (OS.IO.isIn (hd pdl)) 
   1.254 -                                           then
   1.255 -                                               SOME (getCmd (TextIO.inputLine fromStr))
   1.256 -                                           else
   1.257 -                                               NONE
   1.258 -                                   end
   1.259 -                                 else
   1.260 -                                     NONE
   1.261 -                                 end
   1.262 -                             else 
   1.263 -                                 NONE
   1.264 -                            end
   1.265 +	       fun pollChildInput (fromStr) = 
   1.266 +		     let val iod = getInIoDesc fromStr
   1.267 +		     in 
   1.268 +		     if isSome iod 
   1.269 +		     then 
   1.270 +			 let val pd = OS.IO.pollDesc (valOf iod)
   1.271 +			 in 
   1.272 +			 if (isSome pd ) then 
   1.273 +			     let val pd' = OS.IO.pollIn (valOf pd)
   1.274 +				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
   1.275 +			     in
   1.276 +				if null pdl 
   1.277 +				then
   1.278 +				   NONE
   1.279 +				else if (OS.IO.isIn (hd pdl)) 
   1.280 +				     then
   1.281 +					 SOME (getCmd (TextIO.inputLine fromStr))
   1.282 +				     else
   1.283 +					 NONE
   1.284 +			     end
   1.285 +			   else
   1.286 +			       NONE
   1.287 +			   end
   1.288 +		       else 
   1.289 +			   NONE
   1.290 +		      end
   1.291  
   1.292  
   1.293 -                   (****************************************************************************)
   1.294 -                   (* Check all vampire processes currently running for output                 *)
   1.295 -                   (****************************************************************************) 
   1.296 -                                                              (*********************************)
   1.297 -                    fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   1.298 -                                                              (*********************************)
   1.299 -                    |   checkChildren ((childProc::otherChildren), toParentStr) = 
   1.300 -                                            let val (childInput,childOutput) =  cmdstreamsOf childProc
   1.301 -                                                val child_handle= cmdchildHandle childProc
   1.302 -                                                (* childCmd is the .dfg file that the problem is in *)
   1.303 -                                                val childCmd = fst(snd (cmdchildInfo childProc))
   1.304 -                                                (* now get the number of the subgoal from the filename *)
   1.305 -                                                val sg_num = int_of_string(get_nth 5 (rev(explode childCmd)))
   1.306 -                                                val childIncoming = pollChildInput childInput
   1.307 -                                                val parentID = Posix.ProcEnv.getppid()
   1.308 -                                                val prover = cmdProver childProc
   1.309 -                                                val thmstring = cmdThm childProc
   1.310 -                                                val sign = sign_of_thm thm
   1.311 -                                                val prems = prems_of thm
   1.312 -                                                val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.313 -                                                val _ = (warning ("subgoals forked to checkChildren: "^prems_string));
   1.314 -                                                val goalstring = cmdGoal childProc
   1.315 -                                                                                                       
   1.316 -                                                val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));  
   1.317 -                                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
   1.318 -                                                val _ =  TextIO.closeOut outfile
   1.319 -                                            in 
   1.320 -                                              if (isSome childIncoming) 
   1.321 -                                              then 
   1.322 -                                                  (* check here for prover label on child*)
   1.323 -                                                   
   1.324 -                                                  let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
   1.325 -                                                val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) )
   1.326 -                                                val _ =  TextIO.closeOut outfile
   1.327 -                                              val childDone = (case prover of
   1.328 -                                    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   1.329 -                                                   in
   1.330 -                                                    if childDone      (**********************************************)
   1.331 -                                                    then              (* child has found a proof and transferred it *)
   1.332 -                                                                      (**********************************************)
   1.333 +	     (****************************************************************************)
   1.334 +	     (* Check all vampire processes currently running for output                 *)
   1.335 +	     (****************************************************************************) 
   1.336 +							(*********************************)
   1.337 +	      fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   1.338 +							(*********************************)
   1.339 +	      |   checkChildren ((childProc::otherChildren), toParentStr) = 
   1.340 +		    let val (childInput,childOutput) =  cmdstreamsOf childProc
   1.341 +			val child_handle= cmdchildHandle childProc
   1.342 +			(* childCmd is the .dfg file that the problem is in *)
   1.343 +			val childCmd = fst(snd (cmdchildInfo childProc))
   1.344 +			(* now get the number of the subgoal from the filename *)
   1.345 +			val sg_num = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
   1.346 +			val childIncoming = pollChildInput childInput
   1.347 +			val parentID = Posix.ProcEnv.getppid()
   1.348 +			val prover = cmdProver childProc
   1.349 +			val thmstring = cmdThm childProc
   1.350 +			val sign = sign_of_thm thm
   1.351 +			val prems = prems_of thm
   1.352 +			val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.353 +			val _ = (warning ("subgoals forked to checkChildren: "^prems_string));
   1.354 +			val goalstring = cmdGoal childProc
   1.355 +									       
   1.356 +			val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));  
   1.357 +			val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
   1.358 +			val _ =  TextIO.closeOut outfile
   1.359 +		    in 
   1.360 +		      if (isSome childIncoming) 
   1.361 +		      then 
   1.362 +			  (* check here for prover label on child*)
   1.363 +			   
   1.364 +			  let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
   1.365 +			val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) )
   1.366 +			val _ =  TextIO.closeOut outfile
   1.367 +		      val childDone = (case prover of
   1.368 +	    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   1.369 +			   in
   1.370 +			    if childDone      (**********************************************)
   1.371 +			    then              (* child has found a proof and transferred it *)
   1.372 +					      (**********************************************)
   1.373  
   1.374 -                                                       (**********************************************)
   1.375 -                                                       (* Remove this child and go on to check others*)
   1.376 -                                                       (**********************************************)
   1.377 -                                                       ( Unix.reap child_handle;
   1.378 -                                                         checkChildren(otherChildren, toParentStr))
   1.379 -                                                    else 
   1.380 -                                                       (**********************************************)
   1.381 -                                                       (* Keep this child and go on to check others  *)
   1.382 -                                                       (**********************************************)
   1.383 +			       (**********************************************)
   1.384 +			       (* Remove this child and go on to check others*)
   1.385 +			       (**********************************************)
   1.386 +			       ( Unix.reap child_handle;
   1.387 +				 checkChildren(otherChildren, toParentStr))
   1.388 +			    else 
   1.389 +			       (**********************************************)
   1.390 +			       (* Keep this child and go on to check others  *)
   1.391 +			       (**********************************************)
   1.392  
   1.393 -                                                         (childProc::(checkChildren (otherChildren, toParentStr)))
   1.394 -                                                 end
   1.395 -                                               else
   1.396 -                                                   let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
   1.397 -                                                val _ = TextIO.output (outfile,"No child output " )
   1.398 -                                                val _ =  TextIO.closeOut outfile
   1.399 -                                                 in
   1.400 -                                                    (childProc::(checkChildren (otherChildren, toParentStr)))
   1.401 -                                                 end
   1.402 -                                            end
   1.403 +				 (childProc::(checkChildren (otherChildren, toParentStr)))
   1.404 +			 end
   1.405 +		       else
   1.406 +			   let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
   1.407 +			val _ = TextIO.output (outfile,"No child output " )
   1.408 +			val _ =  TextIO.closeOut outfile
   1.409 +			 in
   1.410 +			    (childProc::(checkChildren (otherChildren, toParentStr)))
   1.411 +			 end
   1.412 +		    end
   1.413  
   1.414 -                   
   1.415 -                (********************************************************************)                  
   1.416 -                (* call resolution processes                                        *)
   1.417 -                (* settings should be a list of strings                             *)
   1.418 -                (* e.g. ["-t 300", "-m 100000"]                                     *)
   1.419 -                (* takes list of (string, string, string list, string)list proclist *)
   1.420 -                (********************************************************************)
   1.421 +	     
   1.422 +	  (********************************************************************)                  
   1.423 +	  (* call resolution processes                                        *)
   1.424 +	  (* settings should be a list of strings                             *)
   1.425 +	  (* e.g. ["-t 300", "-m 100000"]                                     *)
   1.426 +	  (* takes list of (string, string, string list, string)list proclist *)
   1.427 +	  (********************************************************************)
   1.428  
   1.429  
   1.430 -  (*** add subgoal id num to this *)
   1.431 -                   fun execCmds  [] procList = procList
   1.432 -                   |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
   1.433 -                                                     if (prover = "spass") 
   1.434 -                                                     then 
   1.435 -                                                         let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   1.436 - 						             val (instr, outstr)=Unix.streamsOf childhandle
   1.437 -                                                             val newProcList =    (((CMDPROC{
   1.438 -            									  prover = prover,
   1.439 -   										  cmd = file,
   1.440 -  									          thmstring = thmstring,
   1.441 -  									          goalstring = goalstring,
   1.442 - 										  proc_handle = childhandle,
   1.443 -									          instr = instr,
   1.444 -   									          outstr = outstr })::procList))
   1.445 -  	                                                      val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child")));  
   1.446 -                                                val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file )
   1.447 -                                                val _ =  TextIO.closeOut outfile
   1.448 -                                                         in
   1.449 -                                                            execCmds cmds newProcList
   1.450 -                                                         end
   1.451 -                                                     else 
   1.452 -                                                         let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   1.453 - 						             val (instr, outstr)=Unix.streamsOf childhandle
   1.454 -							     val newProcList =    (((CMDPROC{
   1.455 -            									  prover = prover,
   1.456 -   										  cmd = file,
   1.457 -  									          thmstring = thmstring,
   1.458 -  									          goalstring = goalstring,
   1.459 - 										  proc_handle = childhandle,
   1.460 -									          instr = instr,
   1.461 -   									          outstr = outstr })::procList))
   1.462 -                                                         in
   1.463 -                                                            execCmds cmds newProcList
   1.464 -                                                         end
   1.465 +(*** add subgoal id num to this *)
   1.466 +	     fun execCmds  [] procList = procList
   1.467 +	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
   1.468 +					       if (prover = "spass") 
   1.469 +					       then 
   1.470 +						   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   1.471 +						       val (instr, outstr)=Unix.streamsOf childhandle
   1.472 +						       val newProcList =    (((CMDPROC{
   1.473 +									    prover = prover,
   1.474 +									    cmd = file,
   1.475 +									    thmstring = thmstring,
   1.476 +									    goalstring = goalstring,
   1.477 +									    proc_handle = childhandle,
   1.478 +									    instr = instr,
   1.479 +									    outstr = outstr })::procList))
   1.480 +							val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child")));  
   1.481 +					  val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file )
   1.482 +					  val _ =  TextIO.closeOut outfile
   1.483 +						   in
   1.484 +						      execCmds cmds newProcList
   1.485 +						   end
   1.486 +					       else 
   1.487 +						   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   1.488 +						       val (instr, outstr)=Unix.streamsOf childhandle
   1.489 +						       val newProcList =    (((CMDPROC{
   1.490 +									    prover = prover,
   1.491 +									    cmd = file,
   1.492 +									    thmstring = thmstring,
   1.493 +									    goalstring = goalstring,
   1.494 +									    proc_handle = childhandle,
   1.495 +									    instr = instr,
   1.496 +									    outstr = outstr })::procList))
   1.497 +						   in
   1.498 +						      execCmds cmds newProcList
   1.499 +						   end
   1.500  
   1.501  
   1.502  
   1.503 -                (****************************************)                  
   1.504 -                (* call resolution processes remotely   *)
   1.505 -                (* settings should be a list of strings *)
   1.506 -                (* e.g. ["-t 300", "-m 100000"]         *)
   1.507 -                (****************************************)
   1.508 -  
   1.509 -                 (*  fun execRemoteCmds  [] procList = procList
   1.510 -                   |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   1.511 -                                             let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   1.512 -                                                 in
   1.513 -                                                      execRemoteCmds  cmds newProcList
   1.514 -                                                 end
   1.515 +	  (****************************************)                  
   1.516 +	  (* call resolution processes remotely   *)
   1.517 +	  (* settings should be a list of strings *)
   1.518 +	  (* e.g. ["-t 300", "-m 100000"]         *)
   1.519 +	  (****************************************)
   1.520 +
   1.521 +	   (*  fun execRemoteCmds  [] procList = procList
   1.522 +	     |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   1.523 +				       let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   1.524 +					   in
   1.525 +						execRemoteCmds  cmds newProcList
   1.526 +					   end
   1.527  *)
   1.528  
   1.529 -                   fun printList (outStr, []) = ()
   1.530 -                   |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   1.531 +	     fun printList (outStr, []) = ()
   1.532 +	     |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   1.533  
   1.534  
   1.535 -                (**********************************************)                  
   1.536 -                (* Watcher Loop                               *)
   1.537 -                (**********************************************)
   1.538 +	  (**********************************************)                  
   1.539 +	  (* Watcher Loop                               *)
   1.540 +	  (**********************************************)
   1.541 +
   1.542  
   1.543  
   1.544  
   1.545 -   
   1.546 -                    fun keepWatching (toParentStr, fromParentStr,procList) = 
   1.547 -                          let    fun loop (procList) =  
   1.548 -                                 (
   1.549 -                                 let val cmdsFromIsa = pollParentInput ()
   1.550 -                                     fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
   1.551 -                                                  TextIO.flushOut toParentStr;
   1.552 -                                                   killChildren (map (cmdchildHandle) procList);
   1.553 -                                                    ())
   1.554 -                                     
   1.555 -                                 in 
   1.556 -                                    (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   1.557 -                                                                                       (**********************************)
   1.558 -                                    if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
   1.559 -                                         (                                             (**********************************)                             
   1.560 -                                          if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   1.561 -                                          then 
   1.562 -                                            (
   1.563 -                                              let val child_handles = map cmdchildHandle procList 
   1.564 -                                              in
   1.565 -                                                 killChildren child_handles;
   1.566 -                                                 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                                              loop ([])
   1.567 -                                              end
   1.568 -                                                 
   1.569 -                                             )
   1.570 -                                          else
   1.571 -                                            ( 
   1.572 -                                              if ((length procList)<10)    (********************)
   1.573 -                                              then                        (* Execute locally  *)
   1.574 -                                                 (                        (********************)
   1.575 -                                                  let 
   1.576 -                                                    val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.577 -                                                    val parentID = Posix.ProcEnv.getppid()
   1.578 -                                                    val newProcList' =checkChildren (newProcList, toParentStr) 
   1.579 -                                                  in
   1.580 -                                                    (*Posix.Process.sleep (Time.fromSeconds 1);*)
   1.581 -                                                    loop (newProcList') 
   1.582 -                                                  end
   1.583 -                                                  )
   1.584 -                                              else                         (*********************************)
   1.585 -                                                                           (* Execute remotely              *)
   1.586 - 									   (* (actually not remote for now )*)
   1.587 -                                                  (                        (*********************************)
   1.588 -                                                  let 
   1.589 -                                                    val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.590 -                                                    val parentID = Posix.ProcEnv.getppid()
   1.591 -                                                    val newProcList' =checkChildren (newProcList, toParentStr) 
   1.592 -                                                  in
   1.593 -                                                    (*Posix.Process.sleep (Time.fromSeconds 1);*)
   1.594 -                                                    loop (newProcList') 
   1.595 -                                                  end
   1.596 -                                                  )
   1.597 +	      fun keepWatching (toParentStr, fromParentStr,procList) = 
   1.598 +		    let    fun loop (procList) =  
   1.599 +			   (
   1.600 +			   let val cmdsFromIsa = pollParentInput ()
   1.601 +			       fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
   1.602 +					    TextIO.flushOut toParentStr;
   1.603 +					     killChildren (map (cmdchildHandle) procList);
   1.604 +					      ())
   1.605 +			       
   1.606 +			   in 
   1.607 +			      (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   1.608 +										 (**********************************)
   1.609 +			      if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
   1.610 +				   (                                             (**********************************)                             
   1.611 +				    if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   1.612 +				    then 
   1.613 +				      (
   1.614 +					let val child_handles = map cmdchildHandle procList 
   1.615 +					in
   1.616 +					   killChildren child_handles;
   1.617 +					   (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                                              loop ([])
   1.618 +					end
   1.619 +					   
   1.620 +				       )
   1.621 +				    else
   1.622 +				      ( 
   1.623 +					if ((length procList)<10)    (********************)
   1.624 +					then                        (* Execute locally  *)
   1.625 +					   (                        (********************)
   1.626 +					    let 
   1.627 +					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.628 +					      val parentID = Posix.ProcEnv.getppid()
   1.629 +					      val newProcList' =checkChildren (newProcList, toParentStr) 
   1.630 +					    in
   1.631 +					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   1.632 +					      loop (newProcList') 
   1.633 +					    end
   1.634 +					    )
   1.635 +					else                         (*********************************)
   1.636 +								     (* Execute remotely              *)
   1.637 +								     (* (actually not remote for now )*)
   1.638 +					    (                        (*********************************)
   1.639 +					    let 
   1.640 +					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.641 +					      val parentID = Posix.ProcEnv.getppid()
   1.642 +					      val newProcList' =checkChildren (newProcList, toParentStr) 
   1.643 +					    in
   1.644 +					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   1.645 +					      loop (newProcList') 
   1.646 +					    end
   1.647 +					    )
   1.648  
   1.649  
   1.650  
   1.651 -                                              )
   1.652 -                                           )                                              (******************************)
   1.653 -                                    else                                                  (* No new input from Isabelle *)
   1.654 -                                                                                          (******************************)
   1.655 -                                        (    let val newProcList = checkChildren ((procList), toParentStr)
   1.656 -                                             in
   1.657 -                                               Posix.Process.sleep (Time.fromSeconds 1);
   1.658 -                                               loop (newProcList)
   1.659 -                                             end
   1.660 -                                         
   1.661 -                                         )
   1.662 -                                  end)
   1.663 -                          in  
   1.664 -                              loop (procList)
   1.665 -                          end
   1.666 -                      
   1.667 -          
   1.668 -                      in
   1.669 -                       (***************************)
   1.670 -                       (*** Sort out pipes ********)
   1.671 -                       (***************************)
   1.672 +					)
   1.673 +				     )                                              (******************************)
   1.674 +			      else                                                  (* No new input from Isabelle *)
   1.675 +										    (******************************)
   1.676 +				  (    let val newProcList = checkChildren ((procList), toParentStr)
   1.677 +				       in
   1.678 +					 Posix.Process.sleep (Time.fromSeconds 1);
   1.679 +					 loop (newProcList)
   1.680 +				       end
   1.681 +				   
   1.682 +				   )
   1.683 +			    end)
   1.684 +		    in  
   1.685 +			loop (procList)
   1.686 +		    end
   1.687 +		
   1.688 +    
   1.689 +		in
   1.690 +		 (***************************)
   1.691 +		 (*** Sort out pipes ********)
   1.692 +		 (***************************)
   1.693  
   1.694 -			Posix.IO.close (#outfd p1);
   1.695 -			Posix.IO.close (#infd p2);
   1.696 -			Posix.IO.dup2{old = oldchildin, new = fromParent};
   1.697 -                        Posix.IO.close oldchildin;
   1.698 -			Posix.IO.dup2{old = oldchildout, new = toParent};
   1.699 -                        Posix.IO.close oldchildout;
   1.700 +		  Posix.IO.close (#outfd p1);
   1.701 +		  Posix.IO.close (#infd p2);
   1.702 +		  Posix.IO.dup2{old = oldchildin, new = fromParent};
   1.703 +		  Posix.IO.close oldchildin;
   1.704 +		  Posix.IO.dup2{old = oldchildout, new = toParent};
   1.705 +		  Posix.IO.close oldchildout;
   1.706  
   1.707 -                        (***************************)
   1.708 -                        (* start the watcher loop  *)
   1.709 -                        (***************************)
   1.710 -                        keepWatching (toParentStr, fromParentStr, procList);
   1.711 +		  (***************************)
   1.712 +		  (* start the watcher loop  *)
   1.713 +		  (***************************)
   1.714 +		  keepWatching (toParentStr, fromParentStr, procList);
   1.715  
   1.716  
   1.717 -                        (****************************************************************************)
   1.718 -                        (* fake return value - actually want the watcher to loop until killed       *)
   1.719 -                        (****************************************************************************)
   1.720 -                        Posix.Process.wordToPid 0w0
   1.721 -			
   1.722 -		      end);
   1.723 -		(* end case *)
   1.724 +		  (****************************************************************************)
   1.725 +		  (* fake return value - actually want the watcher to loop until killed       *)
   1.726 +		  (****************************************************************************)
   1.727 +		  Posix.Process.wordToPid 0w0
   1.728 +		  
   1.729 +		end);
   1.730 +	  (* end case *)
   1.731  
   1.732  
   1.733 -          val _ = TextIO.flushOut TextIO.stdOut
   1.734 +    val _ = TextIO.flushOut TextIO.stdOut
   1.735  
   1.736 -          (*******************************)
   1.737 -          (***  set watcher going ********)
   1.738 -          (*******************************)
   1.739 +    (*******************************)
   1.740 +    (***  set watcher going ********)
   1.741 +    (*******************************)
   1.742  
   1.743 -          val procList = []
   1.744 -          val pid = startWatcher (procList)
   1.745 -          (**************************************************)
   1.746 -          (* communication streams to watcher               *)
   1.747 -          (**************************************************)
   1.748 +    val procList = []
   1.749 +    val pid = startWatcher (procList)
   1.750 +    (**************************************************)
   1.751 +    (* communication streams to watcher               *)
   1.752 +    (**************************************************)
   1.753  
   1.754 -	  val instr = openInFD ("_exec_in", #infd p2)
   1.755 -          val outstr = openOutFD ("_exec_out", #outfd p1)
   1.756 -          
   1.757 -          in
   1.758 -           (*******************************)
   1.759 -           (* close the child-side fds    *)
   1.760 -           (*******************************)
   1.761 -            Posix.IO.close (#outfd p2);
   1.762 -            Posix.IO.close (#infd p1);
   1.763 -            (* set the fds close on exec *)
   1.764 -            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   1.765 -            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   1.766 -             
   1.767 -           (*******************************)
   1.768 -           (* return value                *)
   1.769 -           (*******************************)
   1.770 -            PROC{pid = pid,
   1.771 -              instr = instr,
   1.772 -              outstr = outstr
   1.773 -            }
   1.774 -         end;
   1.775 +    val instr = openInFD ("_exec_in", #infd p2)
   1.776 +    val outstr = openOutFD ("_exec_out", #outfd p1)
   1.777 +    
   1.778 +    in
   1.779 +     (*******************************)
   1.780 +     (* close the child-side fds    *)
   1.781 +     (*******************************)
   1.782 +      Posix.IO.close (#outfd p2);
   1.783 +      Posix.IO.close (#infd p1);
   1.784 +      (* set the fds close on exec *)
   1.785 +      Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   1.786 +      Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   1.787 +       
   1.788 +     (*******************************)
   1.789 +     (* return value                *)
   1.790 +     (*******************************)
   1.791 +      PROC{pid = pid,
   1.792 +	instr = instr,
   1.793 +	outstr = outstr
   1.794 +      }
   1.795 +   end;
   1.796  
   1.797  
   1.798