# HG changeset patch # User paulson # Date 1127390988 -7200 # Node ID c272b91b619f6364267475db6ef7f11e123a9404 # Parent df49216dc5926e0a33cc3e009a7ffbdf7e0ac959 removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements diff -r df49216dc592 -r c272b91b619f src/HOL/Tools/ATP/AtpCommunication.ML --- a/src/HOL/Tools/ATP/AtpCommunication.ML Thu Sep 22 14:02:14 2005 +0200 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML Thu Sep 22 14:09:48 2005 +0200 @@ -87,9 +87,7 @@ (TextIO.output (toParent, msg); TextIO.output (toParent, goalstring^"\n"); TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - (*Space apart signals arising from multiple subgoals*) - Posix.Process.sleep(Time.fromMilliseconds 200)); + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)); (*Called from watcher. Returns true if the Vampire process has returned a verdict.*) fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) = diff -r df49216dc592 -r c272b91b619f src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Sep 22 14:02:14 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Sep 22 14:09:48 2005 +0200 @@ -301,9 +301,7 @@ TextIO.output (toParent, "goalstring: "^goalstring^"\n"); TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1); () + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2) end handle exn => (*FIXME: exn handler is too general!*) (File.write(File.tmp_path (Path.basic "proverString_handler")) @@ -312,9 +310,7 @@ remove_linebreaks proofstr ^ "\n"); TextIO.output (toParent, remove_linebreaks goalstring ^ "\n"); TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1); ()); + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)); val e_lemma_list = prover_lemma_list_aux get_axiom_names_e; @@ -383,10 +379,8 @@ TextIO.output (toParent, reconstr^"\n"); TextIO.output (toParent, goalstring^"\n"); TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1) ; all_tac + all_tac end handle exn => (*FIXME: exn handler is too general!*) (File.append(File.tmp_path (Path.basic "prover_reconstruction")) @@ -395,9 +389,7 @@ (remove_linebreaks proofstr) ^"\n"); TextIO.output (toParent, goalstring^"\n"); TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1); all_tac) + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac) (**********************************************************************************) (* At other end, want to turn back into datatype so can apply reconstruct_proof. *) @@ -699,10 +691,8 @@ val _ = File.append (File.tmp_path (Path.basic "apply_res_1")) ("str is: "^str^" goalstr is: "^goalstring^"\n") val (frees,recon_steps) = parse_step tokens - val isar_str = to_isar_proof (frees, recon_steps, goalstring) - val foo = File.write (File.tmp_path (Path.basic "apply_res_2")) isar_str in - Pretty.writeln(Pretty.str isar_str) + to_isar_proof (frees, recon_steps, goalstring) end end; diff -r df49216dc592 -r c272b91b619f src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Thu Sep 22 14:02:14 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Thu Sep 22 14:09:48 2005 +0200 @@ -45,6 +45,9 @@ val goals_being_watched = ref 0; +val trace_path = Path.basic "watcher_trace"; + + (* The result of calling createWatcher *) datatype proc = PROC of { pid : Posix.Process.pid, @@ -261,6 +264,14 @@ end | NONE => NONE; +(*get the number of the subgoal from the filename: the last digit string*) +fun number_from_filename s = + case String.tokens (not o Char.isDigit) s of + [] => (File.append (File.tmp_path trace_path) + "\nWatcher could not read subgoal nunber!!"; + raise ERROR) + | numbers => valOf (Int.fromString (List.last numbers)); + fun setupWatcher (thm,clause_arr) = let (** pipes for communication between parent and watcher **) @@ -292,7 +303,7 @@ fun pollChildInput fromStr = let val _ = File.append (File.tmp_path (Path.basic "child_poll")) - ("In child_poll\n") + ("\nIn child_poll") val iod = getInIoDesc fromStr in if isSome iod @@ -321,52 +332,35 @@ else NONE end - val cc_iterations_left = ref 50; - (*FIXME: why does this loop if not explicitly bounded?*) - (* Check all ATP processes currently running for output *) (*********************************) fun checkChildren ([], toParentStr) = [] (*** no children to check ********) (*********************************) | checkChildren ((childProc::otherChildren), toParentStr) = - let val _ = File.append (File.tmp_path (Path.basic "child_check")) - ("In check child, length of queue:"^ - Int.toString (length (childProc::otherChildren)) ^ - "\niterations left = " ^ Int.toString (!cc_iterations_left)) - val _ = Posix.Process.sleep (Time.fromMilliseconds 50) (*slow the looping*) + let val _ = File.append (File.tmp_path trace_path) + ("\nIn check child, length of queue:"^ + Int.toString (length (childProc::otherChildren))) val (childInput,childOutput) = cmdstreamsOf childProc val child_handle = cmdchildHandle childProc (* childCmd is the .dfg file that the problem is in *) val childCmd = fst(snd (cmdchildInfo childProc)) - val _ = File.append (File.tmp_path (Path.basic "child_check")) + val _ = File.append (File.tmp_path trace_path) ("\nchildCmd = " ^ childCmd) - (* now get the number of the subgoal from the filename *) - val path_parts = String.tokens(fn c => c = #"/") childCmd - val digits = String.translate - (fn c => if Char.isDigit c then str c else "") - (List.last path_parts); - val sg_num = - (case Int.fromString digits of SOME n => n - | NONE => (File.append (File.tmp_path (Path.basic "child_check")) - "\nWatcher could not read subgoal nunber!!"; - raise ERROR)); + val sg_num = number_from_filename childCmd val childIncoming = pollChildInput childInput - val _ = File.append (File.tmp_path (Path.basic "child_check")) + val _ = File.append (File.tmp_path trace_path) "\nfinished polling child" val parentID = Posix.ProcEnv.getppid() val prover = cmdProver childProc val prems_string = prems_string_of thm val goalstring = cmdGoal childProc - val _ = File.append (File.tmp_path (Path.basic "child_check")) - ("\nsubgoals forked to checkChildren: " ^ - space_implode "\n" [prems_string,prover,goalstring]) + val _ = File.append (File.tmp_path trace_path) + ("\nsubgoals forked to checkChildren: " ^ goalstring) in - cc_iterations_left := !cc_iterations_left - 1; - if !cc_iterations_left = 0 then [] (*Abandon looping!*) - else if isSome childIncoming + if isSome childIncoming then (* check here for prover label on child*) - let val _ = File.append (File.tmp_path (Path.basic "child_check")) + let val _ = File.append (File.tmp_path trace_path) ("\nInput available from childIncoming" ^ "\nchecking if proof found." ^ "\nchildCmd is " ^ childCmd ^ @@ -389,8 +383,8 @@ (childProc::(checkChildren (otherChildren, toParentStr))) end else - (File.append (File.tmp_path (Path.basic "child_check")) - "No child output"; + (File.append (File.tmp_path trace_path) + "\nNo child output"; childProc::(checkChildren (otherChildren, toParentStr))) end @@ -427,7 +421,6 @@ ("\nFinished at " ^ Date.toString(Date.fromTimeLocal(Time.now()))) in - Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList end @@ -449,12 +442,11 @@ (**********************************************) (* Watcher Loop *) (**********************************************) - val iterations_left = ref 100; (*don't let it run forever*) + val iterations_left = ref 500; (*don't let it run forever*) fun keepWatching (procList) = let fun loop procList = - let val _ = Posix.Process.sleep (Time.fromMilliseconds 200) - val _ = File.append (File.tmp_path (Path.basic "keep_watch")) + let val _ = File.append (File.tmp_path trace_path) ("\nCalling pollParentInput: " ^ Int.toString (!iterations_left)); val cmdsFromIsa = pollParentInput @@ -463,11 +455,12 @@ iterations_left := !iterations_left - 1; if !iterations_left <= 0 then (*Sadly, this code fails to terminate the watcher!*) - (File.append (File.tmp_path (Path.basic "keep_watch")) + (File.append (File.tmp_path trace_path) "\nTimeout: Killing proof processes"; TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); TextIO.flushOut toParentStr; - killChildren (map cmdchildHandle procList)) + killChildren (map cmdchildHandle procList); + exit 0) else if isSome cmdsFromIsa then (* deal with input from Isabelle *) if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" @@ -483,11 +476,11 @@ let val newProcList = execCmds (valOf cmdsFromIsa) procList val _ = Posix.ProcEnv.getppid() - val _ = File.append (File.tmp_path (Path.basic "keep_watch")) + val _ = File.append (File.tmp_path trace_path) "\nJust execed a child" val newProcList' = checkChildren (newProcList, toParentStr) in - File.append (File.tmp_path (Path.basic "keep_watch")) + File.append (File.tmp_path trace_path) ("\nOff to keep watching: " ^ Int.toString (!iterations_left)); loop newProcList' @@ -504,7 +497,7 @@ else (* No new input from Isabelle *) let val newProcList = checkChildren (procList, toParentStr) in - File.append (File.tmp_path (Path.basic "keep_watch")) + File.append (File.tmp_path trace_path) ("\nNo new input, still watching: " ^ Int.toString (!iterations_left)); loop newProcList @@ -604,38 +597,24 @@ "\ngoals_being_watched: "^ Int.toString (!goals_being_watched)) 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")); + then (tracing (Recon_Transfer.apply_res_thm outcome goalstring); decr_watched()) 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) - ^ "is not provable")); - Pretty.writeln(Pretty.str (oct_char "361")); + then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "is not provable"); decr_watched()) else if String.isPrefix "Failure" outcome - then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) - ^ "proof attempt failed")); - Pretty.writeln(Pretty.str (oct_char "361")); + then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "proof attempt failed"); decr_watched()) (* print out a list of rules used from clasimpset*) else if String.isPrefix "Success" outcome - then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str (goalstring^outcome)); - Pretty.writeln(Pretty.str (oct_char "361")); + then (tracing (goalstring^outcome); decr_watched()) (* if proof translation failed *) else if String.isPrefix "Translation failed" outcome - then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks outcome))); - Pretty.writeln(Pretty.str (oct_char "361")); + then (tracing (goalstring ^ Recon_Transfer.restore_linebreaks outcome); decr_watched()) else - (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str ("System error in proof handler")); - Pretty.writeln(Pretty.str (oct_char "361")); + (tracing "System error in proof handler"; decr_watched()) end in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);