1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Oct 05 10:56:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Oct 05 11:18:06 2005 +0200
     1.3 @@ -50,6 +50,8 @@
     1.4  (* a special version of repeat_RS *)
     1.5  fun repeat_someI_ex th = repeat_RS th someI_ex;
     1.6  
     1.7 +fun writeln_strs _   []      = ()
     1.8 +  | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
     1.9  
    1.10  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
    1.11  fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
    1.12 @@ -61,8 +63,8 @@
    1.13        val arity_cls = map ResClause.tptp_arity_clause arity_clauses
    1.14        val out = TextIO.openOut(pf n)
    1.15      in
    1.16 -      ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    1.17 -      ResLib.writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
    1.18 +      writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    1.19 +      writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
    1.20        TextIO.closeOut out
    1.21      end;
    1.22  
    1.23 @@ -74,7 +76,7 @@
    1.24                          axclauses [] [] []    
    1.25  	val out = TextIO.openOut(pf n)
    1.26      in
    1.27 -	ResLib.writeln_strs out [probN]; TextIO.closeOut out
    1.28 +	writeln_strs out [probN]; TextIO.closeOut out
    1.29      end;
    1.30  
    1.31  
    1.32 @@ -82,19 +84,20 @@
    1.33  (* call prover with settings and problem file for the current subgoal *)
    1.34  (*********************************************************************)
    1.35  (* now passing in list of skolemized thms and list of sgterms to go with them *)
    1.36 -fun watcher_call_provers sign sg_terms (childin, childout,pid) =
    1.37 +fun watcher_call_provers sign sg_terms (childin, childout, pid) =
    1.38    let
    1.39      fun make_atp_list [] n = []
    1.40        | make_atp_list (sg_term::xs) n =
    1.41            let
    1.42              val goalstring = Sign.string_of_term sign sg_term
    1.43 -            val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
    1.44              val probfile = prob_pathname n
    1.45              val time = Int.toString (!time_limit)
    1.46 -            val _ = debug ("problem file in watcher_call_provers is " ^ probfile)
    1.47            in
    1.48 +            debug ("goalstring in make_atp_lists is\n" ^ goalstring);
    1.49 +            debug ("problem file in watcher_call_provers is " ^ probfile);
    1.50              (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
    1.51                versions of Unix.execute treat them differently!*)
    1.52 +            (*options are separated by Watcher.setting_sep, currently #"%"*)
    1.53              if !prover = "spass"
    1.54              then
    1.55                let val optionline = 
    1.56 @@ -165,7 +168,8 @@
    1.57  	    ())
    1.58        in writenext (length prems); clause_arr end;
    1.59  
    1.60 -val last_watcher_pid = ref (NONE : Posix.Process.pid option);
    1.61 +val last_watcher_pid =
    1.62 +  ref (NONE : (TextIO.instream * TextIO.outstream * Posix.Process.pid) option);
    1.63  
    1.64  
    1.65  (*writes out the current clasimpset to a tptp file;
    1.66 @@ -175,8 +179,13 @@
    1.67    if Thm.no_prems th then ()
    1.68    else
    1.69      let
    1.70 +      val _ = (*Set up signal handler to tidy away dead processes*)
    1.71 +	      IsaSignal.signal (IsaSignal.chld, 
    1.72 +	        IsaSignal.SIG_HANDLE (fn _ =>
    1.73 +		  (Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []);
    1.74 +		   debug "Child signal received\n")));  
    1.75        val _ = (case !last_watcher_pid of NONE => ()
    1.76 -               | SOME pid => (*FIXME: should kill ATP processes too; at least they time out*)
    1.77 +               | SOME (_, childout, pid) => 
    1.78                    (debug ("Killing old watcher, pid = " ^ 
    1.79                            Int.toString (ResLib.intOfPid pid));
    1.80                     Watcher.killWatcher pid))
    1.81 @@ -184,7 +193,7 @@
    1.82        val clause_arr = write_problem_files prob_pathname (ctxt,th)
    1.83        val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr)
    1.84      in
    1.85 -      last_watcher_pid := SOME pid;
    1.86 +      last_watcher_pid := SOME (childin, childout, pid);
    1.87        debug ("proof state: " ^ string_of_thm th);
    1.88        debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
    1.89        watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
    1.90 @@ -208,9 +217,9 @@
    1.91          handle Proof.STATE _ => error "No goal present";
    1.92      val thy = ProofContext.theory_of ctxt;
    1.93    in
    1.94 -    debug ("initial thm in isar_atp: " ^ 
    1.95 +    debug ("initial thm in isar_atp:\n" ^ 
    1.96             Pretty.string_of (ProofContext.pretty_thm ctxt goal));
    1.97 -    debug ("subgoals in isar_atp: " ^ 
    1.98 +    debug ("subgoals in isar_atp:\n" ^ 
    1.99             Pretty.string_of (ProofContext.pretty_term ctxt
   1.100               (Logic.mk_conjunction_list (Thm.prems_of goal))));
   1.101      debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal));