removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
--- 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) =
--- 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;
--- 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);