further tidying; killing of old Watcher loops
authorpaulson
Tue Sep 20 13:17:55 2005 +0200 (2005-09-20)
changeset 175028836793df947
parent 17501 acbebb72e85a
child 17503 b053d5a89b6f
further tidying; killing of old Watcher loops
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue Sep 20 13:17:55 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Tue Sep 20 13:17:55 2005 +0200
     1.3 @@ -115,8 +115,6 @@
     1.4  	    TextIO.StreamIO.mkInstream (
     1.5  	      fdReader (name, fd), ""));
     1.6  
     1.7 -fun killChild child_handle = Unix.reap child_handle 
     1.8 -
     1.9  fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
    1.10  
    1.11  fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
    1.12 @@ -272,6 +270,8 @@
    1.13  fun prems_string_of th =
    1.14    Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
    1.15  
    1.16 +fun killChildren procs = List.app (ignore o Unix.reap) procs;
    1.17 +
    1.18  fun setupWatcher (thm,clause_arr) = 
    1.19    let
    1.20      (** pipes for communication between parent and watcher **)
    1.21 @@ -300,9 +300,6 @@
    1.22  	   val fromParentStr = openInFD ("_exec_in_parent", fromParent)
    1.23  	   val toParentStr = openOutFD ("_exec_out_parent", toParent)
    1.24  	   val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
    1.25 -	   fun killChildren [] = ()
    1.26 -	|      killChildren  (child_handle::children) =
    1.27 -	         (killChild child_handle; killChildren children)
    1.28  
    1.29  	 (*************************************************************)
    1.30  	 (* take an instream and poll its underlying reader for input *)
    1.31 @@ -485,15 +482,13 @@
    1.32  	   let fun loop procList =  
    1.33  		let val _ = Posix.Process.sleep (Time.fromMilliseconds 200)
    1.34  		    val cmdsFromIsa = pollParentInput ()
    1.35 -		    fun killchildHandler ()  = 
    1.36 -			  (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
    1.37 -			   TextIO.flushOut toParentStr;
    1.38 -			   killChildren (map cmdchildHandle procList);
    1.39 -			   ())
    1.40  		in 
    1.41 -		   (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
    1.42  		   iterations_left := !iterations_left - 1;
    1.43 -		   if !iterations_left = 0 then killchildHandler ()
    1.44 +		   if !iterations_left = 0 
    1.45 +		   then (*Sadly, this code fails to terminate the watcher!*)
    1.46 +		    (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
    1.47 +		     TextIO.flushOut toParentStr;
    1.48 +		     killChildren (map cmdchildHandle procList))
    1.49  		   else if isSome cmdsFromIsa
    1.50  		   then (*  deal with input from Isabelle *)
    1.51  		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
    1.52 @@ -501,7 +496,6 @@
    1.53  		       let val child_handles = map cmdchildHandle procList 
    1.54  		       in
    1.55  			  killChildren child_handles;
    1.56 -			  (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)    
    1.57  			  loop []
    1.58  		       end
    1.59  		     else
    1.60 @@ -614,7 +608,7 @@
    1.61  fun createWatcher (thm, clause_arr) =
    1.62   let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
    1.63       fun decr_watched() =
    1.64 -	  (goals_being_watched := (!goals_being_watched) - 1;
    1.65 +	  (goals_being_watched := !goals_being_watched - 1;
    1.66  	   if !goals_being_watched = 0
    1.67  	   then 
    1.68  	     (File.append (File.tmp_path (Path.basic "reap_found"))
    1.69 @@ -629,13 +623,12 @@
    1.70  	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
    1.71  		        "\"\ngoalstring = " ^ goalstring ^
    1.72  		        "\ngoals_being_watched: "^ string_of_int (!goals_being_watched))
    1.73 -       in (* if a proof has been found and sent back as a reconstruction proof *)
    1.74 -	 if String.isPrefix "[" outcome
    1.75 +       in 
    1.76 +	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
    1.77  	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.78  	       Recon_Transfer.apply_res_thm outcome goalstring;
    1.79  	       Pretty.writeln(Pretty.str  (oct_char "361"));
    1.80  	       decr_watched())
    1.81 -	 (* if there's no proof, but a message from the signalling process*)
    1.82  	 else if String.isPrefix "Invalid" outcome
    1.83  	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.84  	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) 
     2.1 --- a/src/HOL/Tools/res_atp.ML	Tue Sep 20 13:17:55 2005 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Sep 20 13:17:55 2005 +0200
     2.3 @@ -60,11 +60,7 @@
     2.4  fun repeat_someI_ex thm = repeat_RS thm someI_ex;
     2.5  
     2.6  
     2.7 -(*********************************************************************)
     2.8 -(* write out a subgoal as tptp clauses to the file "probN"           *)
     2.9 -(* where N is the number of this subgoal                             *)
    2.10 -(*********************************************************************)
    2.11 -
    2.12 +(* write out a subgoal as tptp clauses to the file "xxxx_N"*)
    2.13  fun tptp_inputs_tfrees thms n axclauses =
    2.14      let
    2.15        val _ = debug ("in tptp_inputs_tfrees 0")
    2.16 @@ -83,22 +79,16 @@
    2.17        debug probfile
    2.18      end;
    2.19  
    2.20 -
    2.21 -(*********************************************************************)
    2.22 -(* write out a subgoal as DFG clauses to the file "probN"           *)
    2.23 -(* where N is the number of this subgoal                             *)
    2.24 -(*********************************************************************)
    2.25 -
    2.26 +(* write out a subgoal in DFG format to the file "xxxx_N"*)
    2.27  fun dfg_inputs_tfrees thms n axclauses = 
    2.28      let val clss = map (ResClause.make_conjecture_clause_thm) thms
    2.29          val probfile = prob_pathname() ^ "_" ^ (string_of_int n)
    2.30          val _ = debug ("about to write out dfg prob file " ^ probfile)
    2.31 -        val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
    2.32 +        val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ string_of_int n)
    2.33                          axclauses [] [] []    
    2.34  	val out = TextIO.openOut(probfile)
    2.35      in
    2.36  	(ResLib.writeln_strs out [probN]; TextIO.closeOut out; debug probfile )
    2.37 -(* (ResLib.writeln_strs out (tfree_clss @ dfg_clss); *)
    2.38      end;
    2.39  
    2.40  
    2.41 @@ -115,7 +105,7 @@
    2.42              val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
    2.43  
    2.44              val probfile = prob_pathname() ^ "_" ^ string_of_int n
    2.45 -            val _ = debug ("prob file in watcher_call_provers is " ^ probfile)
    2.46 +            val _ = debug ("problem file in watcher_call_provers is " ^ probfile)
    2.47            in
    2.48              (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
    2.49                versions of Unix.execute treat them differently!*)
    2.50 @@ -175,8 +165,7 @@
    2.51               all_tac))]) n thm;
    2.52          ());
    2.53  
    2.54 -
    2.55 -(*FIXME: WHAT IS THMS FOR????*)
    2.56 +val last_watcher_pid = ref (NONE : Posix.Process.pid option);
    2.57  
    2.58  (******************************************************************)
    2.59  (* called in Isar automatically                                   *)
    2.60 @@ -185,16 +174,21 @@
    2.61  (******************************************************************)
    2.62  (*FIX changed to clasimp_file *)
    2.63  val isar_atp = setmp print_mode [] 
    2.64 - (fn (ctxt, thms, thm) =>
    2.65 + (fn (ctxt, thm) =>
    2.66    if Thm.no_prems thm then ()
    2.67    else
    2.68      let
    2.69        val _= debug ("in isar_atp")
    2.70        val thy = ProofContext.theory_of ctxt
    2.71        val prems = Thm.prems_of thm
    2.72 -      val thms_string = Meson.concat_with_and (map string_of_thm thms)
    2.73        val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
    2.74  
    2.75 +      val _ = (case !last_watcher_pid of NONE => ()
    2.76 +               | SOME pid => (*FIXME: should kill ATP processes too; at least they time out*)
    2.77 +                  (debug ("Killing old watcher, pid = " ^ 
    2.78 +                          Int.toString (ResLib.intOfPid pid));
    2.79 +                   Watcher.killWatcher pid))
    2.80 +              handle OS.SysErr _ => debug "Attempt to kill watcher failed";
    2.81        (*set up variables for writing out the clasimps to a tptp file*)
    2.82        val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
    2.83                (*FIXME: hack!! need to consider relevance for all prems*)
    2.84 @@ -202,7 +196,7 @@
    2.85                       string_of_int (Array.length clause_arr))
    2.86        val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr)
    2.87      in
    2.88 -      debug ("initial thms: " ^ thms_string);
    2.89 +      last_watcher_pid := SOME pid;
    2.90        debug ("subgoals: " ^ prems_string);
    2.91        debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
    2.92        write_problem_files axclauses thm (length prems);
    2.93 @@ -210,7 +204,7 @@
    2.94      end);
    2.95  
    2.96  val isar_atp_writeonly = setmp print_mode [] 
    2.97 - (fn (ctxt, thms: thm list, thm) =>
    2.98 + (fn (ctxt, thm) =>
    2.99    if Thm.no_prems thm then ()
   2.100    else
   2.101      let val prems = Thm.prems_of thm
   2.102 @@ -220,23 +214,6 @@
   2.103      end);
   2.104  
   2.105  
   2.106 -(* convert locally declared rules to axiom clauses: UNUSED *)
   2.107 -
   2.108 -fun subtract_simpset thy ctxt =
   2.109 -  let
   2.110 -    val rules1 = #rules (#1 (rep_ss (simpset_of thy)));
   2.111 -    val rules2 = #rules (#1 (rep_ss (local_simpset_of ctxt)));
   2.112 -  in map #thm (Net.subtract MetaSimplifier.eq_rrule rules1 rules2) end;
   2.113 -
   2.114 -fun subtract_claset thy ctxt =
   2.115 -  let
   2.116 -    val (netI1, netE1) = #xtra_netpair (rep_cs (claset_of thy));
   2.117 -    val (netI2, netE2) = #xtra_netpair (rep_cs (local_claset_of ctxt));
   2.118 -    val subtract = map (#2 o #2) oo Net.subtract Tactic.eq_kbrl;
   2.119 -  in subtract netI1 netI2 @ subtract netE1 netE2 end;
   2.120 -
   2.121 -
   2.122 -
   2.123  (** the Isar toplevel hook **)
   2.124  
   2.125  val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   2.126 @@ -256,8 +233,8 @@
   2.127      hook_count := !hook_count +1;
   2.128      debug ("in hook for time: " ^(string_of_int (!hook_count)) );
   2.129      ResClause.init thy;
   2.130 -    if !destdir = "" then isar_atp (ctxt, ProofContext.prems_of ctxt, goal)
   2.131 -    else isar_atp_writeonly (ctxt, ProofContext.prems_of ctxt, goal)
   2.132 +    if !destdir = "" then isar_atp (ctxt, goal)
   2.133 +    else isar_atp_writeonly (ctxt, goal)
   2.134    end);
   2.135  
   2.136  val call_atpP =