# HG changeset patch # User paulson # Date 1127215075 -7200 # Node ID 8836793df94741e335e35dfb62f37a589af4de30 # Parent acbebb72e85a556fbb374e2a3f4dd74f3fe1f1e2 further tidying; killing of old Watcher loops diff -r acbebb72e85a -r 8836793df947 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Tue Sep 20 13:17:55 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Tue Sep 20 13:17:55 2005 +0200 @@ -115,8 +115,6 @@ TextIO.StreamIO.mkInstream ( fdReader (name, fd), "")); -fun killChild child_handle = Unix.reap child_handle - fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr)); fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr); @@ -272,6 +270,8 @@ fun prems_string_of th = Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th)) +fun killChildren procs = List.app (ignore o Unix.reap) procs; + fun setupWatcher (thm,clause_arr) = let (** pipes for communication between parent and watcher **) @@ -300,9 +300,6 @@ val fromParentStr = openInFD ("_exec_in_parent", fromParent) val toParentStr = openOutFD ("_exec_out_parent", toParent) val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm); - fun killChildren [] = () - | killChildren (child_handle::children) = - (killChild child_handle; killChildren children) (*************************************************************) (* take an instream and poll its underlying reader for input *) @@ -485,15 +482,13 @@ let fun loop procList = let val _ = Posix.Process.sleep (Time.fromMilliseconds 200) val cmdsFromIsa = pollParentInput () - fun killchildHandler () = - (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); - TextIO.flushOut toParentStr; - killChildren (map cmdchildHandle procList); - ()) in - (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*) iterations_left := !iterations_left - 1; - if !iterations_left = 0 then killchildHandler () + if !iterations_left = 0 + then (*Sadly, this code fails to terminate the watcher!*) + (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); + TextIO.flushOut toParentStr; + killChildren (map cmdchildHandle procList)) else if isSome cmdsFromIsa then (* deal with input from Isabelle *) if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" @@ -501,7 +496,6 @@ let val child_handles = map cmdchildHandle procList in killChildren child_handles; - (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) loop [] end else @@ -614,7 +608,7 @@ fun createWatcher (thm, clause_arr) = let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr)) fun decr_watched() = - (goals_being_watched := (!goals_being_watched) - 1; + (goals_being_watched := !goals_being_watched - 1; if !goals_being_watched = 0 then (File.append (File.tmp_path (Path.basic "reap_found")) @@ -629,13 +623,12 @@ val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ "\"\ngoalstring = " ^ goalstring ^ "\ngoals_being_watched: "^ string_of_int (!goals_being_watched)) - in (* if a proof has been found and sent back as a reconstruction proof *) - if String.isPrefix "[" outcome + in + if String.isPrefix "[" outcome (*indicates a proof reconstruction*) then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); Recon_Transfer.apply_res_thm outcome goalstring; Pretty.writeln(Pretty.str (oct_char "361")); decr_watched()) - (* if there's no proof, but a message from the signalling process*) else if String.isPrefix "Invalid" outcome then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) diff -r acbebb72e85a -r 8836793df947 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Tue Sep 20 13:17:55 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Tue Sep 20 13:17:55 2005 +0200 @@ -60,11 +60,7 @@ fun repeat_someI_ex thm = repeat_RS thm someI_ex; -(*********************************************************************) -(* write out a subgoal as tptp clauses to the file "probN" *) -(* where N is the number of this subgoal *) -(*********************************************************************) - +(* write out a subgoal as tptp clauses to the file "xxxx_N"*) fun tptp_inputs_tfrees thms n axclauses = let val _ = debug ("in tptp_inputs_tfrees 0") @@ -83,22 +79,16 @@ debug probfile end; - -(*********************************************************************) -(* write out a subgoal as DFG clauses to the file "probN" *) -(* where N is the number of this subgoal *) -(*********************************************************************) - +(* write out a subgoal in DFG format to the file "xxxx_N"*) fun dfg_inputs_tfrees thms n axclauses = let val clss = map (ResClause.make_conjecture_clause_thm) thms val probfile = prob_pathname() ^ "_" ^ (string_of_int n) val _ = debug ("about to write out dfg prob file " ^ probfile) - val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) + val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ string_of_int n) axclauses [] [] [] val out = TextIO.openOut(probfile) in (ResLib.writeln_strs out [probN]; TextIO.closeOut out; debug probfile ) -(* (ResLib.writeln_strs out (tfree_clss @ dfg_clss); *) end; @@ -115,7 +105,7 @@ val _ = debug ("goalstring in make_atp_lists is " ^ goalstring) val probfile = prob_pathname() ^ "_" ^ string_of_int n - val _ = debug ("prob file in watcher_call_provers is " ^ probfile) + val _ = debug ("problem file in watcher_call_provers is " ^ probfile) in (*Avoid command arguments containing spaces: Poly/ML and SML/NJ versions of Unix.execute treat them differently!*) @@ -175,8 +165,7 @@ all_tac))]) n thm; ()); - -(*FIXME: WHAT IS THMS FOR????*) +val last_watcher_pid = ref (NONE : Posix.Process.pid option); (******************************************************************) (* called in Isar automatically *) @@ -185,16 +174,21 @@ (******************************************************************) (*FIX changed to clasimp_file *) val isar_atp = setmp print_mode [] - (fn (ctxt, thms, thm) => + (fn (ctxt, thm) => if Thm.no_prems thm then () else let val _= debug ("in isar_atp") val thy = ProofContext.theory_of ctxt val prems = Thm.prems_of thm - val thms_string = Meson.concat_with_and (map string_of_thm thms) val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems) + val _ = (case !last_watcher_pid of NONE => () + | SOME pid => (*FIXME: should kill ATP processes too; at least they time out*) + (debug ("Killing old watcher, pid = " ^ + Int.toString (ResLib.intOfPid pid)); + Watcher.killWatcher pid)) + handle OS.SysErr _ => debug "Attempt to kill watcher failed"; (*set up variables for writing out the clasimps to a tptp file*) val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) (*FIXME: hack!! need to consider relevance for all prems*) @@ -202,7 +196,7 @@ string_of_int (Array.length clause_arr)) val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr) in - debug ("initial thms: " ^ thms_string); + last_watcher_pid := SOME pid; debug ("subgoals: " ^ prems_string); debug ("pid: " ^ Int.toString (ResLib.intOfPid pid)); write_problem_files axclauses thm (length prems); @@ -210,7 +204,7 @@ end); val isar_atp_writeonly = setmp print_mode [] - (fn (ctxt, thms: thm list, thm) => + (fn (ctxt, thm) => if Thm.no_prems thm then () else let val prems = Thm.prems_of thm @@ -220,23 +214,6 @@ end); -(* convert locally declared rules to axiom clauses: UNUSED *) - -fun subtract_simpset thy ctxt = - let - val rules1 = #rules (#1 (rep_ss (simpset_of thy))); - val rules2 = #rules (#1 (rep_ss (local_simpset_of ctxt))); - in map #thm (Net.subtract MetaSimplifier.eq_rrule rules1 rules2) end; - -fun subtract_claset thy ctxt = - let - val (netI1, netE1) = #xtra_netpair (rep_cs (claset_of thy)); - val (netI2, netE2) = #xtra_netpair (rep_cs (local_claset_of ctxt)); - val subtract = map (#2 o #2) oo Net.subtract Tactic.eq_kbrl; - in subtract netI1 netI2 @ subtract netE1 netE2 end; - - - (** the Isar toplevel hook **) val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state => @@ -256,8 +233,8 @@ hook_count := !hook_count +1; debug ("in hook for time: " ^(string_of_int (!hook_count)) ); ResClause.init thy; - if !destdir = "" then isar_atp (ctxt, ProofContext.prems_of ctxt, goal) - else isar_atp_writeonly (ctxt, ProofContext.prems_of ctxt, goal) + if !destdir = "" then isar_atp (ctxt, goal) + else isar_atp_writeonly (ctxt, goal) end); val call_atpP =