# HG changeset patch # User paulson # Date 1127990716 -7200 # Node ID 9dab1e491d105fe99a94ab89c5d1b5ad561b467c # Parent 7c6a96cbc96636b6635999d5ab89e6e26ea34021 reduction in tracing files diff -r 7c6a96cbc966 -r 9dab1e491d10 src/HOL/Tools/ATP/AtpCommunication.ML --- a/src/HOL/Tools/ATP/AtpCommunication.ML Thu Sep 29 12:45:04 2005 +0200 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML Thu Sep 29 12:45:16 2005 +0200 @@ -27,6 +27,11 @@ (* switch for whether to reconstruct a proof found, or just list the lemmas used *) val reconstruct = ref false; +val trace_path = Path.basic "atp_trace"; + +fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s + else (); + exception EOF; val start_E = "# Proof object starts here." @@ -64,18 +69,17 @@ let val thisLine = TextIO.inputLine fromChild in if thisLine = "" (*end of file?*) - then (File.write (File.tmp_path (Path.basic"extraction_failed")) - ("end bracket: " ^ endS ^ - "\naccumulated text: " ^ currentString); + then (trace ("\n extraction_failed. End bracket: " ^ endS ^ + "\naccumulated text: " ^ currentString); raise EOF) else if String.isPrefix endS thisLine then let val proofextract = extract_proof (currentString^thisLine) + val lemma_list = if endS = end_V8 + then Recon_Transfer.vamp_lemma_list + else Recon_Transfer.e_lemma_list in - File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; - (if endS = end_V8 (*vampire?*) - then Recon_Transfer.vamp_lemma_list - else Recon_Transfer.e_lemma_list) - proofextract goalstring toParent ppid clause_arr + trace ("\nExtracted_prf\n" ^ proofextract); + lemma_list proofextract goalstring toParent ppid clause_arr end else transferInput (currentString^thisLine) end @@ -87,17 +91,16 @@ (TextIO.output (toParent, msg); TextIO.output (toParent, goalstring^"\n"); TextIO.flushOut toParent; + trace ("\nSignalled parent: " ^ msg); 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) = let val thisLine = TextIO.inputLine fromChild in - File.append (File.tmp_path (Path.basic "proof")) thisLine; + trace thisLine; if thisLine = "" - then (File.append (File.tmp_path (Path.basic "proof")) - "No proof output seen \n"; - false) + then (trace "No proof output seen\n"; false) else if String.isPrefix start_V8 thisLine then startTransfer (end_V8, fromChild, toParent, ppid, goalstring, childCmd, clause_arr) @@ -114,11 +117,9 @@ fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, clause_arr) = let val thisLine = TextIO.inputLine fromChild in - File.append (File.tmp_path (Path.basic "proof")) thisLine; + trace thisLine; if thisLine = "" - then (File.append (File.tmp_path (Path.basic "proof")) - "No proof output seen \n"; - false) + 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) @@ -152,13 +153,13 @@ let val thisLine = TextIO.inputLine fromChild in if thisLine = "" (*end of file?*) - then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString; + then (trace ("\nspass_extraction_failed: " ^ currentString); raise EOF) else if String.isPrefix "--------------------------SPASS-STOP" thisLine then let val proofextract = extract_proof (currentString^thisLine) in - File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; + trace ("\nextracted spass proof: " ^ proofextract); if !reconstruct then (spass_reconstruct_tac proofextract goalstring toParent ppid sg_num clause_arr thm; ()) @@ -182,8 +183,7 @@ in if thisLine = "" then false else if String.isPrefix "Here is a proof" thisLine then - (File.append (File.tmp_path (Path.basic "spass_transfer")) - ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n"); + (trace ("\nabout to transfer proof, thm is " ^ string_of_thm thm); transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine, thm, sg_num,clause_arr); true) handle EOF => false @@ -192,40 +192,26 @@ end -(*Called from watcher. Returns true if the E process has returned a verdict.*) +(*Called from watcher. Returns true if the SPASS process has returned a verdict.*) fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd, thm, sg_num, clause_arr) = - let val spass_proof_file = TextIO.openAppend - (File.platform_path(File.tmp_path (Path.basic "spass_proof"))) - val thisLine = TextIO.inputLine fromChild + let val thisLine = TextIO.inputLine fromChild in - File.write (File.tmp_path (Path.basic "spass_response")) thisLine; - if thisLine = "" - then (TextIO.output (spass_proof_file, ("No proof output seen \n")); - TextIO.closeOut spass_proof_file; - false) + trace thisLine; + 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) else if thisLine = "SPASS beiseite: Completion found.\n" - then - (TextIO.output (spass_proof_file, thisLine); - TextIO.closeOut spass_proof_file; - signal_parent (toParent, ppid, "Invalid\n", goalstring); - true) + then (signal_parent (toParent, ppid, "Invalid\n", goalstring); + 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); - TextIO.output (spass_proof_file, "signalled parent\n"); - TextIO.closeOut spass_proof_file; - true) - else - (TextIO.output (spass_proof_file, thisLine); - TextIO.flushOut spass_proof_file; - checkSpassProofFound (fromChild, toParent, ppid, goalstring, - childCmd, thm, sg_num, clause_arr)) + then (signal_parent (toParent, ppid, "Failure\n", goalstring); + true) + else checkSpassProofFound (fromChild, toParent, ppid, goalstring, + childCmd, thm, sg_num, clause_arr) end end; diff -r 7c6a96cbc966 -r 9dab1e491d10 src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Sep 29 12:45:04 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Sep 29 12:45:16 2005 +0200 @@ -10,6 +10,11 @@ infixr 8 ++; infixr 7 >>; infixr 6 ||; +val trace_path = Path.basic "transfer_trace"; + +fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s + else (); + (* Versions that include type information *) @@ -175,11 +180,9 @@ fun get_axiom_names_spass proofstr clause_arr = let (* parse spass proof into datatype *) - val _ = File.write (File.tmp_path (Path.basic "parsing_progress")) - ("Started parsing:\n" ^ proofstr) - val tokens = #1(lex proofstr) - val proof_steps = parse tokens - val _ = File.append (File.tmp_path (Path.basic "parsing_progress")) "\nFinished!" + val _ = trace ("\nStarted parsing:\n" ^ proofstr) + val proof_steps = parse (#1(lex proofstr)) + val _ = trace "\nParsing finished!" (* get axioms as correctly numbered clauses w.r.t. the Spass proof *) in get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr @@ -248,8 +251,8 @@ val meta_strs = map ReconOrderClauses.get_meta_lits metas val metas_and_strs = ListPair.zip (metas,meta_strs) - val _ = File.write(File.tmp_path (Path.basic "foo_clauses")) (onestr ax_strs) - val _ = File.write(File.tmp_path (Path.basic "foo_metastrs")) (onestr meta_strs) + val _ = trace ("\nAxioms: " ^ onestr ax_strs) + val _ = trace ("\nMeta_strs: " ^ onestr meta_strs) (* get list of axioms as thms with their variables *) @@ -283,25 +286,23 @@ fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr = - let val _ = File.append(File.tmp_path (Path.basic "prover_lemmastring")) - ("proofstr is " ^ proofstr ^ + let val _ = trace + ("\nGetting lemma names. proofstr is " ^ proofstr ^ "\ngoalstr is " ^ goalstring ^ "\nnum 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 - File.append(File.tmp_path (Path.basic "prover_lemmastring")) - ("\nlemma list is: " ^ ax_str); + trace ("\nDone. Lemma list is " ^ ax_str); TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^ ax_str ^ "\n"); TextIO.output (toParent, "goalstring: "^goalstring^"\n"); TextIO.flushOut toParent; - 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")) - ("In exception handler: " ^ Toplevel.exn_message exn); + (trace ("\nprover_lemma_list_aux: In exception handler: " ^ + Toplevel.exn_message exn); TextIO.output (toParent, "Translation failed for the proof: " ^ remove_linebreaks proofstr ^ "\n"); TextIO.output (toParent, remove_linebreaks goalstring ^ "\n"); @@ -318,17 +319,13 @@ (**** Full proof reconstruction for SPASS (not really working) ****) fun spass_reconstruct proofstr goalstring toParent ppid thms clause_arr = - let val _ = File.write(File.tmp_path (Path.basic "prover_reconstruction")) - ("proofstr is: "^proofstr) + let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr) val tokens = #1(lex proofstr) - (***********************************) (* parse spass proof into datatype *) (***********************************) val proof_steps = parse tokens - - val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) - ("Did parsing on "^proofstr) + val _ = trace "\nParsing finished" (************************************) (* recreate original subgoal as thm *) @@ -341,17 +338,15 @@ val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr (*val numcls_string = numclstr ( vars, numcls) ""*) - val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) "got axioms" + val _ = trace "\ngot axioms" (************************************) (* translate proof *) (************************************) - val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) - ("about to translate proof, steps: " - ^(init_proofsteps_to_string proof_steps "")) + val _ = trace ("\nabout to translate proof, steps: " + ^ (init_proofsteps_to_string proof_steps "")) val (newthm,proof) = translate_proof numcls proof_steps vars - val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) - ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")) + val _ = trace ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")) (***************************************************) (* transfer necessary steps as strings to Isabelle *) (***************************************************) @@ -368,9 +363,8 @@ else [] val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) "" val frees_str = "["^(thmvars_to_string frees "")^"]" - val _ = File.write (File.tmp_path (Path.basic "reconstringfile")) - (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr) val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr) + val _ = trace ("\nReconstruction:\n" ^ reconstr) in TextIO.output (toParent, reconstr^"\n"); TextIO.output (toParent, goalstring^"\n"); @@ -379,8 +373,7 @@ all_tac end handle exn => (*FIXME: exn handler is too general!*) - (File.append(File.tmp_path (Path.basic "prover_reconstruction")) - ("In exception handler: " ^ Toplevel.exn_message exn); + (trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn); TextIO.output (toParent,"Translation failed for the proof:"^ (remove_linebreaks proofstr) ^"\n"); TextIO.output (toParent, goalstring^"\n"); @@ -667,7 +660,7 @@ (isar_lines firststeps "")^ (last_isar_line laststep)^ ("qed") - val _ = File.write (File.tmp_path (Path.basic "isar_proof_file")) isar_proof + val _ = trace ("\nto_isar_proof returns " ^ isar_proof) in isar_proof end; @@ -684,8 +677,7 @@ fun apply_res_thm str goalstring = let val tokens = #1 (lex str); - val _ = File.append (File.tmp_path (Path.basic "apply_res_1")) - ("str is: "^str^" goalstr is: "^goalstring^"\n") + val _ = trace ("\napply_res_thm. str is: "^str^" goalstr is: "^goalstring^"\n") val (frees,recon_steps) = parse_step tokens in to_isar_proof (frees, recon_steps, goalstring)