# HG changeset patch # User paulson # Date 1128586462 -7200 # Node ID 818cec5f82a4131a64a0b5f8236c5af2a7d118c4 # Parent 1e07f6ab3118c996260de152deea203bd8cedaf7 major simplification: removal of the goalstring argument diff -r 1e07f6ab3118 -r 818cec5f82a4 src/HOL/Tools/ATP/AtpCommunication.ML --- 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; diff -r 1e07f6ab3118 -r 818cec5f82a4 src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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; diff -r 1e07f6ab3118 -r 818cec5f82a4 src/HOL/Tools/ATP/watcher.ML --- 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()) diff -r 1e07f6ab3118 -r 818cec5f82a4 src/HOL/Tools/res_atp.ML --- 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))));