src/HOL/Tools/ATP/watcher.ML
changeset 17502 8836793df947
parent 17488 67376a311a2b
child 17525 ae5bb6001afb
     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)