--- a/src/HOL/Tools/ATP/AtpCommunication.ML Thu Oct 06 10:13:34 2005 +0200
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML Thu Oct 06 10:14:22 2005 +0200
@@ -12,13 +12,13 @@
val reconstruct : bool ref
val checkEProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * string * (ResClause.clause * thm) Array.array -> bool
+ string * (ResClause.clause * thm) Array.array -> bool
val checkVampProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * string * (ResClause.clause * thm) Array.array -> bool
+ string * (ResClause.clause * thm) Array.array -> bool
val checkSpassProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * string * thm * int * (ResClause.clause * thm) Array.array -> bool
+ string * thm * int * (ResClause.clause * thm) Array.array -> bool
end;
structure AtpCommunication : ATP_COMMUNICATION =
@@ -64,7 +64,7 @@
(* and if so, transfer output to the input pipe of the main Isabelle process *)
(*********************************************************************************)
-fun startTransfer (endS, fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
+fun startTransfer (endS, fromChild, toParent, ppid, probfile, clause_arr) =
let fun transferInput currentString =
let val thisLine = TextIO.inputLine fromChild
in
@@ -78,8 +78,8 @@
then Recon_Transfer.vamp_lemma_list
else Recon_Transfer.e_lemma_list
in
- trace ("\nExtracted_prf\n" ^ proofextract);
- lemma_list proofextract goalstring toParent ppid clause_arr
+ trace ("\nExtracted proof:\n" ^ proofextract);
+ lemma_list proofextract probfile toParent ppid clause_arr
end
else transferInput (currentString^thisLine)
end
@@ -87,34 +87,35 @@
transferInput ""; true
end handle EOF => false
-fun signal_parent (toParent, ppid, msg, goalstring) =
+
+(*The signal handler in watcher.ML must be able to read the output of this.*)
+fun signal_parent (toParent, ppid, msg, probfile) =
(TextIO.output (toParent, msg);
- TextIO.output (toParent, goalstring);
+ TextIO.output (toParent, probfile ^ "\n");
TextIO.flushOut toParent;
- trace ("\nSignalled parent: " ^ msg);
+ trace ("\nSignalled parent: " ^ msg ^ probfile);
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) =
+fun checkVampProofFound (fromChild, toParent, ppid, probfile, clause_arr) =
let val thisLine = TextIO.inputLine fromChild
in
trace thisLine;
if thisLine = ""
- then (trace "No proof output seen\n"; false)
+ then (trace "\nNo proof output seen"; false)
else if String.isPrefix start_V8 thisLine
- then
- startTransfer (end_V8, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
+ then startTransfer (end_V8, fromChild, toParent, ppid, probfile, clause_arr)
else if (String.isPrefix "Satisfiability detected" thisLine) orelse
(String.isPrefix "Refutation not found" thisLine)
- then (signal_parent (toParent, ppid, "Failure\n", goalstring);
+ then (signal_parent (toParent, ppid, "Failure\n", probfile);
true)
else
- checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
+ checkVampProofFound (fromChild, toParent, ppid, probfile, clause_arr)
end
(*Called from watcher. Returns true if the E process has returned a verdict.*)
-fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, clause_arr) =
+fun checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr) =
let val thisLine = TextIO.inputLine fromChild
in
trace thisLine;
@@ -122,15 +123,15 @@
then (trace "No proof output seen\n"; false)
else if String.isPrefix start_E thisLine
then
- startTransfer (end_E, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
+ startTransfer (end_E, fromChild, toParent, ppid, probfile, clause_arr)
else if String.isPrefix "# Problem is satisfiable" thisLine
- then (signal_parent (toParent, ppid, "Invalid\n", goalstring);
+ then (signal_parent (toParent, ppid, "Invalid\n", probfile);
true)
else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
- then (signal_parent (toParent, ppid, "Failure\n", goalstring);
+ then (signal_parent (toParent, ppid, "Failure\n", probfile);
true)
else
- checkEProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
+ checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr)
end
@@ -140,18 +141,19 @@
(* steps as a string to the input pipe of the main Isabelle process *)
(**********************************************************************)
-fun spass_reconstruct_tac proofextract goalstring toParent ppid sg_num
- clause_arr =
+fun spass_reconstruct_tac proofextract toParent ppid probfile sg_num clause_arr =
SELECT_GOAL
(EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac,
METAHYPS(fn negs =>
- Recon_Transfer.spass_reconstruct proofextract goalstring toParent ppid negs clause_arr)]) sg_num;
+ Recon_Transfer.spass_reconstruct proofextract probfile
+ toParent ppid negs clause_arr)]) sg_num;
-fun transferSpassInput (fromChild, toParent, ppid, goalstring,
+fun transferSpassInput (fromChild, toParent, ppid, probfile,
currentString, thm, sg_num, clause_arr) =
let val thisLine = TextIO.inputLine fromChild
in
+ trace thisLine;
if thisLine = "" (*end of file?*)
then (trace ("\nspass_extraction_failed: " ^ currentString);
raise EOF)
@@ -161,12 +163,12 @@
in
trace ("\nextracted spass proof: " ^ proofextract);
if !reconstruct
- then (spass_reconstruct_tac proofextract goalstring toParent ppid sg_num
+ then (spass_reconstruct_tac proofextract toParent ppid probfile sg_num
clause_arr thm; ())
- else Recon_Transfer.spass_lemma_list proofextract goalstring
- toParent ppid clause_arr
+ else Recon_Transfer.spass_lemma_list proofextract probfile toParent
+ ppid clause_arr
end
- else transferSpassInput (fromChild, toParent, ppid, goalstring,
+ else transferSpassInput (fromChild, toParent, ppid, probfile,
(currentString^thisLine), thm, sg_num, clause_arr)
end;
@@ -177,23 +179,22 @@
(*********************************************************************************)
-fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd,
+fun startSpassTransfer (fromChild, toParent, ppid, probfile,
thm, sg_num,clause_arr) =
let val thisLine = TextIO.inputLine fromChild
in
if thisLine = "" then false
else if String.isPrefix "Here is a proof" thisLine then
- (trace ("\nabout to transfer proof, thm is " ^ string_of_thm thm);
- transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine,
+ (trace ("\nabout to transfer SPASS proof\n:");
+ transferSpassInput (fromChild, toParent, ppid, probfile, thisLine,
thm, sg_num,clause_arr);
true) handle EOF => false
- else startSpassTransfer (fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num,clause_arr)
+ else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,clause_arr)
end
(*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
-fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd,
+fun checkSpassProofFound (fromChild, toParent, ppid, probfile,
thm, sg_num, clause_arr) =
let val thisLine = TextIO.inputLine fromChild
in
@@ -201,17 +202,15 @@
if thisLine = "" then (trace "No proof output seen\n"; false)
else if thisLine = "SPASS beiseite: Proof found.\n"
then
- startSpassTransfer (fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num, clause_arr)
+ startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
else if thisLine = "SPASS beiseite: Completion found.\n"
- then (signal_parent (toParent, ppid, "Invalid\n", goalstring);
+ then (signal_parent (toParent, ppid, "Invalid\n", probfile);
true)
else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
- then (signal_parent (toParent, ppid, "Failure\n", goalstring);
+ then (signal_parent (toParent, ppid, "Failure\n", probfile);
true)
- else checkSpassProofFound (fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num, clause_arr)
+ else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
end
end;
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Oct 06 10:13:34 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Oct 06 10:14:22 2005 +0200
@@ -280,18 +280,19 @@
| rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
-fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr =
+(*The signal handler in watcher.ML must be able to read the output of this.*)
+fun prover_lemma_list_aux getax proofstr probfile toParent ppid clause_arr =
let val _ = trace
("\nGetting lemma names. proofstr is " ^ proofstr ^
- "\ngoalstring is " ^ goalstring ^
- "num of clauses is " ^ string_of_int (Array.length clause_arr))
+ "\nprobfile is " ^ probfile ^
+ " num of clauses is " ^ string_of_int (Array.length clause_arr))
val axiom_names = getax proofstr clause_arr
val ax_str = rules_to_string axiom_names
in
trace ("\nDone. Lemma list is " ^ ax_str);
TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
ax_str ^ "\n");
- TextIO.output (toParent, goalstring);
+ TextIO.output (toParent, probfile ^ "\n");
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
end
@@ -300,7 +301,7 @@
Toplevel.exn_message exn);
TextIO.output (toParent, "Translation failed for the proof: " ^
String.toString proofstr ^ "\n");
- TextIO.output (toParent, goalstring);
+ TextIO.output (toParent, probfile);
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
@@ -313,7 +314,7 @@
(**** Full proof reconstruction for SPASS (not really working) ****)
-fun spass_reconstruct proofstr goalstring toParent ppid thms clause_arr =
+fun spass_reconstruct proofstr probfile toParent ppid thms clause_arr =
let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr)
val tokens = #1(lex proofstr)
@@ -362,16 +363,16 @@
val _ = trace ("\nReconstruction:\n" ^ reconstr)
in
TextIO.output (toParent, reconstr^"\n");
- TextIO.output (toParent, goalstring);
+ TextIO.output (toParent, probfile ^ "\n");
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
all_tac
end
handle exn => (*FIXME: exn handler is too general!*)
(trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn);
- TextIO.output (toParent,"Translation failed for the proof:"^
+ TextIO.output (toParent,"Translation failed for SPASS proof:"^
String.toString proofstr ^"\n");
- TextIO.output (toParent, goalstring);
+ TextIO.output (toParent, probfile ^ "\n");
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac)
@@ -484,19 +485,6 @@
>>(fn (_,(a,_)) => a)
-
-
-fun anytoken_step input = (word>> (fn (a) => a) ) input
- handle NOPARSE_WORD => (number>> (fn (a) => string_of_int a) ) input
- handle NOPARSE_NUMBER => (other_char >> (fn(a) => a)) input
-
-
-
-fun goalstring_step input= (anytoken_step ++ many (anytoken_step )
- >> (fn (a,b) => (a^" "^(implode b)))) input
-
-
-
val linestep = number ++ methodstep ++ term_lists_step ++ term_lists_step
>> (fn (a, (b, (c,d))) => (a,(b,c,d)))
@@ -630,7 +618,7 @@
fun last_isar_line (numb,( step, clstrs,thmstrs)) = "show \"False\"\n"^(by_isar_line step)
-fun to_isar_proof (frees, xs, goalstring) =
+fun to_isar_proof (frees, xs) =
let val extraaxioms = get_extraaxioms xs
val extraax_num = length extraaxioms
val origaxioms_and_steps = Library.drop (extraax_num, xs)
@@ -643,10 +631,9 @@
val steps = Library.drop (origax_num, axioms_and_steps)
val firststeps = ReconOrderClauses.butlast steps
val laststep = List.last steps
- val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
val isar_proof =
- ("show \""^goalstring^"\"\n")^
+ ("show \"[your goal]\"\n")^
("proof (rule ccontr,skolemize, make_clauses) \n")^
("fix "^(frees_to_isar_str frees)^"\n")^
(assume_isar_extraaxioms extraaxioms)^
@@ -670,13 +657,12 @@
(* be passed over to the watcher, e.g. numcls25 *)
(*******************************************************)
-fun apply_res_thm str goalstring =
+fun apply_res_thm str =
let val tokens = #1 (lex str);
- val _ = trace ("\napply_res_thm. str is: "^str^
- "\ngoalstring is: \n"^goalstring^"\n")
+ val _ = trace ("\napply_res_thm. str is: "^str^"\n")
val (frees,recon_steps) = parse_step tokens
in
- to_isar_proof (frees, recon_steps, goalstring)
+ to_isar_proof (frees, recon_steps)
end
end;
--- a/src/HOL/Tools/ATP/watcher.ML Thu Oct 06 10:13:34 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Thu Oct 06 10:14:22 2005 +0200
@@ -17,8 +17,7 @@
(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
val callResProvers :
- TextIO.outstream * (string*string*string*string*string) list
- -> unit
+ TextIO.outstream * (string*string*string*string) list -> unit
(* Send message to watcher to kill resolution provers *)
val callSlayer : TextIO.outstream -> unit
@@ -50,31 +49,18 @@
else ();
(* The result of calling createWatcher *)
-datatype proc = PROC of {
- pid : Posix.Process.pid,
- instr : TextIO.instream,
- outstr : TextIO.outstream
- };
+datatype proc = PROC of {pid : Posix.Process.pid,
+ instr : TextIO.instream,
+ outstr : TextIO.outstream};
(* The result of calling executeToList *)
datatype cmdproc = CMDPROC of {
prover: string, (* Name of the resolution prover used, e.g. Vampire*)
cmd: string, (* The file containing the goal for res prover to prove *)
- goalstring: string, (* string representation of subgoal*)
proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
instr : TextIO.instream, (* Input stream to child process *)
outstr : TextIO.outstream}; (* Output stream from child process *)
-type signal = Posix.Signal.signal
-datatype exit_status = datatype Posix.Process.exit_status
-
-val fromStatus = Posix.Process.fromStatus
-
-fun reap(pid, instr, outstr) =
- let val u = TextIO.closeIn instr;
- val u = TextIO.closeOut outstr;
- val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
- in status end
fun fdReader (name : string, fd : Posix.IO.file_desc) =
Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
@@ -103,17 +89,13 @@
fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
-fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) =
+fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,instr,outstr}) =
(prover,(cmd, (instr,outstr)));
-fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr}) =
+fun cmdchildHandle (CMDPROC{prover,cmd,proc_handle,instr,outstr}) =
proc_handle;
-fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr}) =
- prover;
-
-fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr}) =
- goalstring;
+fun cmdProver (CMDPROC{prover,cmd,proc_handle,instr,outstr}) = prover;
(* gets individual args from instream and concatenates them into a list *)
@@ -136,17 +118,13 @@
fun callResProvers (toWatcherStr, []) =
(TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr)
| callResProvers (toWatcherStr,
- (prover,goalstring, proverCmd,settings,
- probfile) :: args) =
- let val _ = trace (space_implode "\n"
- (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
- probfile]))
+ (prover,proverCmd,settings,probfile) :: args) =
+ let val _ = trace (space_implode ", "
+ (["\ncallResProvers:", prover, proverCmd, probfile]))
in TextIO.output (toWatcherStr,
(*Uses a special character to separate items sent to watcher*)
space_implode (str command_sep)
- [prover, proverCmd, settings, probfile,
- String.toString goalstring ^ "\n"]);
- (*goalstring is a single string literal, with all specials escaped.*)
+ [prover, proverCmd, settings, probfile, "\n"]);
goals_being_watched := (!goals_being_watched) + 1;
TextIO.flushOut toWatcherStr;
callResProvers (toWatcherStr,args)
@@ -172,17 +150,16 @@
else if thisLine = "Kill children\n"
then (TextIO.output (toParentStr,thisLine);
TextIO.flushOut toParentStr;
- [("","","Kill children",[],"")])
+ [("","Kill children",[],"")])
else
- let val [prover,proverCmd,settingstr,probfile,goalstring] =
+ let val [prover,proverCmd,settingstr,probfile,_] =
String.tokens (fn c => c = command_sep) thisLine
val settings = String.tokens (fn c => c = setting_sep) settingstr
in
- trace ("\nprover: " ^ prover ^ " prover path: " ^ proverCmd^
- " problem file: " ^ probfile ^
- "\ngoalstring: "^goalstring);
+ trace ("\nprover: " ^ prover ^ " prover path: " ^ proverCmd ^
+ "\n problem file: " ^ probfile);
getCmds (toParentStr, fromParentStr,
- (prover, goalstring, proverCmd, settings, probfile)::cmdList)
+ (prover, proverCmd, settings, probfile)::cmdList)
end
handle Bind =>
(trace "getCmds: command parsing failed!";
@@ -215,8 +192,7 @@
(* for tracing: encloses each string element in brackets. *)
val concat_with_and = space_implode " & " o map (enclose "(" ")");
-fun prems_string_of th =
- concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
+fun prems_string_of th = concat_with_and (map string_of_cterm (cprems_of th))
fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
@@ -239,13 +215,14 @@
(*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
- [] => (trace "\nWatcher could not read subgoal nunber!!"; raise ERROR)
+ [] => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
+ raise ERROR)
| numbers => valOf (Int.fromString (List.last numbers));
fun setupWatcher (thm,clause_arr) =
let
- val p1 = Posix.IO.pipe () (** pipes for communication between parent and watcher **)
- val p2 = Posix.IO.pipe ()
+ val p1 = Posix.IO.pipe() (*pipes for communication between parent and watcher*)
+ val p2 = Posix.IO.pipe()
fun closep () =
(Posix.IO.close (#outfd p1); Posix.IO.close (#infd p1);
Posix.IO.close (#outfd p2); Posix.IO.close (#infd p2))
@@ -264,7 +241,7 @@
val pid = Posix.ProcEnv.getpid()
val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
(*set process group id: allows killing all children*)
- val () = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
+ val () = trace "\nsubgoals forked to startWatcher"
fun pollChildInput fromStr =
case getInIoDesc fromStr of
@@ -292,18 +269,16 @@
val childIncoming = pollChildInput childInput
val parentID = Posix.ProcEnv.getppid()
val prover = cmdProver childProc
- val prems_string = prems_string_of thm
- val goalstring = cmdGoal childProc
in
- trace("\nsubgoals forked to checkChildren: " ^ goalstring);
if childIncoming
then (* check here for prover label on child*)
let val _ = trace ("\nInput available from child: " ^ childCmd ^
- "\ngoalstring is " ^ goalstring)
+ "\nprover is " ^ prover)
val childDone = (case prover of
- "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)
- | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)
- |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr) )
+ "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID, childCmd, clause_arr)
+ | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID, childCmd, clause_arr)
+ | "spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID, childCmd, thm, sg_num,clause_arr)
+ | _ => (trace "\nBad prover!"; true) )
in
if childDone
then (* child has found a proof and transferred it *)
@@ -323,117 +298,89 @@
(* settings should be a list of strings ["-t 300", "-m 100000"] *)
(* takes list of (string, string, string list, string)list proclist *)
fun execCmds [] procList = procList
- | execCmds ((prover, goalstring,proverCmd,settings,file)::cmds) procList =
- let val _ = trace (space_implode "\n"
- (["\nAbout to execute command for goal:",
- goalstring, proverCmd] @ settings @
- [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
+ | execCmds ((prover,proverCmd,settings,file)::cmds) procList =
+ let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^
+ file)
val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc =
Unix.execute(proverCmd, settings@[file])
val (instr, outstr) = Unix.streamsOf childhandle
val newProcList = CMDPROC{prover = prover,
cmd = file,
- goalstring = goalstring,
proc_handle = childhandle,
instr = instr,
outstr = outstr} :: procList
-
- val _ = trace ("\nFinished at " ^
+ val _ = trace ("\nFinished at " ^
Date.toString(Date.fromTimeLocal(Time.now())))
in execCmds cmds newProcList end
(******** Watcher Loop ********)
- val limit = ref 500; (*don't let it run forever*)
+ val limit = ref 200; (*don't let it run forever*)
fun keepWatching (procList) =
let fun loop procList =
- let val _ = trace ("\nCalling pollParentInput: " ^ Int.toString (!limit));
+ let val _ = trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^
+ " length(procList) = " ^ Int.toString (length procList));
val cmdsFromIsa = pollParentInput
(fromParentIOD, fromParentStr, toParentStr)
in
- OS.Process.sleep (Time.fromMilliseconds 100);
- limit := !limit - 1;
- if !limit = 0
- then
- (trace "\nTimeout: Killing proof processes";
- TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
- TextIO.flushOut toParentStr;
- killChildren (map cmdchildHandle procList);
- exit 0)
- else case cmdsFromIsa of
- SOME [(_,_,"Kill children",_,_)] =>
- let val child_handles = map cmdchildHandle procList
- in killChildren child_handles; loop [] end
- | SOME cmds => (* deal with commands from Isabelle process *)
- if length procList < 40
- then (* Execute locally *)
- let
- val newProcList = execCmds cmds procList
- val newProcList' = checkChildren (newProcList, toParentStr)
- in
- trace "\nJust execed a child"; loop newProcList'
- end
- else (* Execute remotely [FIXME: NOT REALLY] *)
- let
- val newProcList = execCmds cmds procList
- val newProcList' = checkChildren (newProcList, toParentStr)
- in loop newProcList' end
- | NONE => (* No new input from Isabelle *)
- let val newProcList = checkChildren (procList, toParentStr)
- in
- trace "\nNo new input, still watching"; loop newProcList
- end
+ OS.Process.sleep (Time.fromMilliseconds 100);
+ limit := !limit - 1;
+ if !limit = 0
+ then
+ (trace "\nTimeout: Killing proof processes";
+ TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
+ TextIO.flushOut toParentStr;
+ killChildren (map cmdchildHandle procList);
+ Posix.Process.exit 0w0)
+ else case cmdsFromIsa of
+ SOME [(_,"Kill children",_,_)] =>
+ let val child_handles = map cmdchildHandle procList
+ in trace "\nReceived command to kill children";
+ killChildren child_handles; loop []
+ end
+ | SOME cmds => (* deal with commands from Isabelle process *)
+ if length procList < 40
+ then (* Execute locally *)
+ let
+ val _ = trace ("\nCommands from parent: " ^ Int.toString(length cmds))
+ val newProcList = execCmds cmds procList
+ val newProcList' = checkChildren (newProcList, toParentStr)
+ in
+ trace "\nCommands executed"; loop newProcList'
+ end
+ else (* Execute remotely [FIXME: NOT REALLY] *)
+ let
+ val newProcList = execCmds cmds procList
+ val newProcList' = checkChildren (newProcList, toParentStr)
+ in loop newProcList' end
+ | NONE => (* No new input from Isabelle *)
+ let val newProcList = checkChildren (procList, toParentStr)
+ in
+ trace "\nNothing from parent, still watching"; loop newProcList
+ end
end
- in
- loop procList
- end
-
-
+ in loop procList end
in
- (*** Sort out pipes ********)
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p2);
+ (*** Sort out pipes ********)
+ Posix.IO.close (#outfd p1); Posix.IO.close (#infd p2);
Posix.IO.dup2{old = oldchildin, new = fromParent};
Posix.IO.close oldchildin;
Posix.IO.dup2{old = oldchildout, new = toParent};
Posix.IO.close oldchildout;
-
- (* start the watcher loop *)
- keepWatching (procList);
- (* fake return value - actually want the watcher to loop until killed *)
- Posix.Process.wordToPid 0w0
- end);
- (* end case *)
-
+ keepWatching (procList)
+ end); (* end case *)
val _ = TextIO.flushOut TextIO.stdOut
-
- (*******************************)
- (*** set watcher going ********)
- (*******************************)
-
- val procList = []
- val pid = startWatcher procList
- (**************************************************)
- (* communication streams to watcher *)
- (**************************************************)
-
+ val pid = startWatcher []
+ (* communication streams to watcher*)
val instr = openInFD ("_exec_in", #infd p2)
val outstr = openOutFD ("_exec_out", #outfd p1)
-
in
- (*******************************)
- (* close the child-side fds *)
- (*******************************)
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p1);
+ (* close the child-side fds*)
+ Posix.IO.close (#outfd p2); Posix.IO.close (#infd p1);
(* set the fds close on exec *)
Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
-
- (*******************************)
- (* return value *)
- (*******************************)
PROC{pid = pid, instr = instr, outstr = outstr}
end;
@@ -445,12 +392,17 @@
fun killWatcher pid = Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
-fun reapWatcher(pid, instr, outstr) =
+fun reapWatcher(pid, instr, outstr) = ignore
(TextIO.closeIn instr; TextIO.closeOut outstr;
- Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
+ Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
+ handle OS.SysErr _ => ()
-fun createWatcher (thm, clause_arr) =
- let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
+fun string_of_subgoal th i =
+ string_of_cterm (List.nth(cprems_of th, i-1))
+ handle Subscript => "Subgoal number out of range!"
+
+fun createWatcher (th, clause_arr) =
+ let val (childpid,(childin,childout)) = childInfo (setupWatcher(th,clause_arr))
fun decr_watched() =
(goals_being_watched := !goals_being_watched - 1;
if !goals_being_watched = 0
@@ -459,30 +411,32 @@
LargeWord.toString (Posix.Process.pidToWord childpid));
killWatcher childpid; reapWatcher (childpid,childin, childout))
else ())
- val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
+ val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of th);
fun proofHandler n =
let val outcome = TextIO.inputLine childin
- val goalstring = valOf (String.fromString (TextIO.inputLine childin))
+ val probfile = TextIO.inputLine childin
+ val sg_num = number_from_filename probfile
+ val text = string_of_subgoal th sg_num
val _ = debug ("In signal handler. outcome = \"" ^ outcome ^
- "\"\ngoalstring = " ^ goalstring ^
+ "\"\nprobfile = " ^ probfile ^
"\ngoals_being_watched: "^ Int.toString (!goals_being_watched))
in
if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
- then (priority (Recon_Transfer.apply_res_thm outcome goalstring);
+ then (priority (Recon_Transfer.apply_res_thm outcome);
decr_watched())
else if String.isPrefix "Invalid" outcome
- then (priority ("Subgoal is not provable:\n" ^ goalstring);
+ then (priority ("Subgoal is not provable:\n" ^ text);
decr_watched())
else if String.isPrefix "Failure" outcome
- then (priority ("Proof attempt failed:\n" ^ goalstring);
+ then (priority ("Proof attempt failed:\n" ^ text);
decr_watched())
(* print out a list of rules used from clasimpset*)
else if String.isPrefix "Success" outcome
- then (priority (outcome ^ goalstring);
+ then (priority (outcome ^ text);
decr_watched())
(* if proof translation failed *)
else if String.isPrefix "Translation failed" outcome
- then (priority (outcome ^ goalstring);
+ then (priority (outcome ^ text);
decr_watched())
else (priority "System error in proof handler";
decr_watched())
--- a/src/HOL/Tools/res_atp.ML Thu Oct 06 10:13:34 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Thu Oct 06 10:14:22 2005 +0200
@@ -89,11 +89,9 @@
fun make_atp_list [] n = []
| make_atp_list (sg_term::xs) n =
let
- val goalstring = Sign.string_of_term sign sg_term
val probfile = prob_pathname n
val time = Int.toString (!time_limit)
in
- debug ("goalstring in make_atp_lists is\n" ^ goalstring);
debug ("problem file in watcher_call_provers is " ^ probfile);
(*Avoid command arguments containing spaces: Poly/ML and SML/NJ
versions of Unix.execute treat them differently!*)
@@ -111,7 +109,7 @@
val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
(*We've checked that SPASS is there for ATP/spassshell to run.*)
in
- ([("spass", goalstring,
+ ([("spass",
getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
optionline, probfile)] @
(make_atp_list xs (n+1)))
@@ -120,14 +118,14 @@
then
let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vampire"
in
- ([("vampire", goalstring, vampire, "-m 100000%-t " ^ time, probfile)] @
+ ([("vampire", vampire, "-m 100000%-t " ^ time, probfile)] @
(make_atp_list xs (n+1))) (*BEWARE! spaces in options!*)
end
else if !prover = "E"
then
let val Eprover = ResLib.helper_path "E_HOME" "eproof"
in
- ([("E", goalstring, Eprover,
+ ([("E", Eprover,
"--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time,
probfile)] @
(make_atp_list xs (n+1)))
@@ -156,21 +154,20 @@
val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses))
val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees
fun writenext n =
- if n=0 then ()
+ if n=0 then []
else
(SELECT_GOAL
(EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac,
METAHYPS(fn negs =>
(write (make_clauses negs) pf n
(axclauses,classrel_clauses,arity_clauses);
- writenext (n-1);
all_tac))]) n th;
- ())
- in writenext (length prems); clause_arr end;
+ pf n :: writenext (n-1))
+ in (writenext (length prems), clause_arr) end;
val last_watcher_pid =
- ref (NONE : (TextIO.instream * TextIO.outstream * Posix.Process.pid) option);
-
+ ref (NONE : (TextIO.instream * TextIO.outstream *
+ Posix.Process.pid * string list) option);
(*writes out the current clasimpset to a tptp file;
turns off xsymbol at start of function, restoring it at end *)
@@ -179,22 +176,24 @@
if Thm.no_prems th then ()
else
let
- val _ = (*Set up signal handler to tidy away dead processes*)
- IsaSignal.signal (IsaSignal.chld,
- IsaSignal.SIG_HANDLE (fn _ =>
- (Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []);
- debug "Child signal received\n")));
+ fun reap s = (*Signal handler to tidy away dead processes*)
+ (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
+ SOME _ => reap s | NONE => ())
+ handle OS.SysErr _ => ()
+ val _ =
+ IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)
val _ = (case !last_watcher_pid of NONE => ()
- | SOME (_, childout, pid) =>
+ | SOME (_, childout, pid, files) =>
(debug ("Killing old watcher, pid = " ^
Int.toString (ResLib.intOfPid pid));
- Watcher.killWatcher pid))
+ Watcher.killWatcher pid;
+ ignore (map (try OS.FileSys.remove) files)))
handle OS.SysErr _ => debug "Attempt to kill watcher failed";
- val clause_arr = write_problem_files prob_pathname (ctxt,th)
+ val (files,clause_arr) = write_problem_files prob_pathname (ctxt,th)
val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr)
in
- last_watcher_pid := SOME (childin, childout, pid);
- debug ("proof state: " ^ string_of_thm th);
+ last_watcher_pid := SOME (childin, childout, pid, files);
+ debug ("problem files: " ^ space_implode ", " files);
debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
end);
@@ -217,8 +216,6 @@
handle Proof.STATE _ => error "No goal present";
val thy = ProofContext.theory_of ctxt;
in
- debug ("initial thm in isar_atp:\n" ^
- Pretty.string_of (ProofContext.pretty_thm ctxt goal));
debug ("subgoals in isar_atp:\n" ^
Pretty.string_of (ProofContext.pretty_term ctxt
(Logic.mk_conjunction_list (Thm.prems_of goal))));