reduction in tracing files
authorpaulson
Thu Sep 29 12:45:16 2005 +0200 (2005-09-29)
changeset 177189dab1e491d10
parent 17717 7c6a96cbc966
child 17719 2e75155c5ed5
reduction in tracing files
src/HOL/Tools/ATP/AtpCommunication.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
     1.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML	Thu Sep 29 12:45:04 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Thu Sep 29 12:45:16 2005 +0200
     1.3 @@ -27,6 +27,11 @@
     1.4  (* switch for whether to reconstruct a proof found, or just list the lemmas used *)
     1.5  val reconstruct = ref false;
     1.6  
     1.7 +val trace_path = Path.basic "atp_trace";
     1.8 +
     1.9 +fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
    1.10 +              else ();
    1.11 +
    1.12  exception EOF;
    1.13  
    1.14  val start_E = "# Proof object starts here."
    1.15 @@ -64,18 +69,17 @@
    1.16        let val thisLine = TextIO.inputLine fromChild
    1.17        in
    1.18  	if thisLine = "" (*end of file?*)
    1.19 -	then (File.write (File.tmp_path (Path.basic"extraction_failed")) 
    1.20 -	                 ("end bracket: " ^ endS ^
    1.21 -	                  "\naccumulated text: " ^ currentString);
    1.22 +	then (trace ("\n extraction_failed.  End bracket: " ^ endS ^
    1.23 +	             "\naccumulated text: " ^ currentString);
    1.24  	      raise EOF)                    
    1.25  	else if String.isPrefix endS thisLine
    1.26  	then let val proofextract = extract_proof (currentString^thisLine)
    1.27 +	         val lemma_list = if endS = end_V8 
    1.28 +			  	  then Recon_Transfer.vamp_lemma_list
    1.29 +			  	  else Recon_Transfer.e_lemma_list
    1.30  	     in
    1.31 -	       File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; 
    1.32 -	       (if endS = end_V8 (*vampire?*)
    1.33 -		then Recon_Transfer.vamp_lemma_list
    1.34 -		else Recon_Transfer.e_lemma_list)
    1.35 -	           proofextract goalstring toParent ppid clause_arr
    1.36 +	       trace ("\nExtracted_prf\n" ^ proofextract); 
    1.37 +	       lemma_list proofextract goalstring toParent ppid clause_arr
    1.38  	     end
    1.39  	else transferInput (currentString^thisLine)
    1.40        end
    1.41 @@ -87,17 +91,16 @@
    1.42   (TextIO.output (toParent, msg);
    1.43    TextIO.output (toParent, goalstring^"\n");
    1.44    TextIO.flushOut toParent;
    1.45 +  trace ("\nSignalled parent: " ^ msg);
    1.46    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
    1.47  
    1.48  (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
    1.49  fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
    1.50   let val thisLine = TextIO.inputLine fromChild
    1.51   in   
    1.52 -     File.append (File.tmp_path (Path.basic "proof")) thisLine;
    1.53 +     trace thisLine;
    1.54       if thisLine = "" 
    1.55 -     then (File.append (File.tmp_path (Path.basic "proof"))
    1.56 -                      "No proof output seen \n";
    1.57 -	   false)
    1.58 +     then (trace "No proof output seen\n"; false)
    1.59       else if String.isPrefix start_V8 thisLine
    1.60       then
    1.61         startTransfer (end_V8, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
    1.62 @@ -114,11 +117,9 @@
    1.63  fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, clause_arr) = 
    1.64   let val thisLine = TextIO.inputLine fromChild  
    1.65   in   
    1.66 -     File.append (File.tmp_path (Path.basic "proof")) thisLine;
    1.67 +     trace thisLine;
    1.68       if thisLine = "" 
    1.69 -     then (File.append (File.tmp_path (Path.basic "proof"))
    1.70 -                      "No proof output seen \n";
    1.71 -	   false)
    1.72 +     then (trace "No proof output seen\n"; false)
    1.73       else if String.isPrefix start_E thisLine
    1.74       then      
    1.75         startTransfer (end_E, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
    1.76 @@ -152,13 +153,13 @@
    1.77   let val thisLine = TextIO.inputLine fromChild 
    1.78   in 
    1.79      if thisLine = "" (*end of file?*)
    1.80 -    then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString;
    1.81 +    then (trace ("\nspass_extraction_failed: " ^ currentString);
    1.82  	  raise EOF)                    
    1.83      else if String.isPrefix "--------------------------SPASS-STOP" thisLine
    1.84      then 
    1.85        let val proofextract = extract_proof (currentString^thisLine)
    1.86        in 
    1.87 -	 File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract;
    1.88 +	 trace ("\nextracted spass proof: " ^ proofextract);
    1.89  	 if !reconstruct 
    1.90  	 then (spass_reconstruct_tac proofextract goalstring toParent ppid sg_num 
    1.91  		clause_arr thm; ())
    1.92 @@ -182,8 +183,7 @@
    1.93     in                 
    1.94        if thisLine = "" then false
    1.95        else if String.isPrefix "Here is a proof" thisLine then     
    1.96 -	 (File.append (File.tmp_path (Path.basic "spass_transfer"))
    1.97 -		      ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n");
    1.98 +	 (trace ("\nabout to transfer proof, thm is " ^ string_of_thm thm);
    1.99  	  transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine, 
   1.100   	                     thm, sg_num,clause_arr);
   1.101  	  true) handle EOF => false
   1.102 @@ -192,40 +192,26 @@
   1.103      end
   1.104  
   1.105  
   1.106 -(*Called from watcher. Returns true if the E process has returned a verdict.*)
   1.107 +(*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   1.108  fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd,
   1.109                            thm, sg_num, clause_arr) = 
   1.110 - let val spass_proof_file = TextIO.openAppend
   1.111 -           (File.platform_path(File.tmp_path (Path.basic "spass_proof")))
   1.112 -     val thisLine = TextIO.inputLine fromChild  
   1.113 + let val thisLine = TextIO.inputLine fromChild  
   1.114   in    
   1.115 -     File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
   1.116 -     if thisLine = "" 
   1.117 -     then (TextIO.output (spass_proof_file, ("No proof output seen \n"));
   1.118 -	   TextIO.closeOut spass_proof_file;
   1.119 -	   false)
   1.120 +     trace thisLine;
   1.121 +     if thisLine = "" then (trace "No proof output seen\n"; false)
   1.122       else if thisLine = "SPASS beiseite: Proof found.\n"
   1.123       then      
   1.124          startSpassTransfer (fromChild, toParent, ppid, goalstring,
   1.125  	                    childCmd, thm, sg_num, clause_arr)
   1.126       else if thisLine = "SPASS beiseite: Completion found.\n"
   1.127 -     then  
   1.128 -       (TextIO.output (spass_proof_file, thisLine);
   1.129 -	TextIO.closeOut spass_proof_file;
   1.130 -	signal_parent (toParent, ppid, "Invalid\n", goalstring);
   1.131 -	true)
   1.132 +     then (signal_parent (toParent, ppid, "Invalid\n", goalstring);
   1.133 +	   true)
   1.134       else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   1.135               thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   1.136 -     then  
   1.137 -       (signal_parent (toParent, ppid, "Failure\n", goalstring);
   1.138 -	TextIO.output (spass_proof_file, "signalled parent\n");
   1.139 -	TextIO.closeOut spass_proof_file;
   1.140 -	true)
   1.141 -    else
   1.142 -       (TextIO.output (spass_proof_file, thisLine);
   1.143 -       TextIO.flushOut spass_proof_file;
   1.144 -       checkSpassProofFound  (fromChild, toParent, ppid, goalstring,
   1.145 -       childCmd, thm, sg_num, clause_arr))
   1.146 +     then (signal_parent (toParent, ppid, "Failure\n", goalstring);
   1.147 +	   true)
   1.148 +    else checkSpassProofFound (fromChild, toParent, ppid, goalstring,
   1.149 +                          childCmd, thm, sg_num, clause_arr)
   1.150   end
   1.151  
   1.152  end;
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 29 12:45:04 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 29 12:45:16 2005 +0200
     2.3 @@ -10,6 +10,11 @@
     2.4  
     2.5  infixr 8 ++; infixr 7 >>; infixr 6 ||;
     2.6  
     2.7 +val trace_path = Path.basic "transfer_trace";
     2.8 +
     2.9 +fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
    2.10 +              else ();
    2.11 +
    2.12  
    2.13  (* Versions that include type information *)
    2.14   
    2.15 @@ -175,11 +180,9 @@
    2.16  
    2.17  fun get_axiom_names_spass proofstr clause_arr =
    2.18    let (* parse spass proof into datatype *)
    2.19 -      val _ = File.write (File.tmp_path (Path.basic "parsing_progress")) 
    2.20 -                         ("Started parsing:\n" ^ proofstr)
    2.21 -      val tokens = #1(lex proofstr)
    2.22 -      val proof_steps = parse tokens
    2.23 -      val _ = File.append (File.tmp_path (Path.basic "parsing_progress")) "\nFinished!"
    2.24 +      val _ = trace ("\nStarted parsing:\n" ^ proofstr)
    2.25 +      val proof_steps = parse (#1(lex proofstr))
    2.26 +      val _ = trace "\nParsing finished!"
    2.27        (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
    2.28    in
    2.29      get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr
    2.30 @@ -248,8 +251,8 @@
    2.31       val meta_strs = map ReconOrderClauses.get_meta_lits metas
    2.32      
    2.33       val metas_and_strs = ListPair.zip (metas,meta_strs)
    2.34 -     val _ = File.write(File.tmp_path (Path.basic "foo_clauses")) (onestr ax_strs)
    2.35 -     val _ = File.write(File.tmp_path (Path.basic "foo_metastrs")) (onestr meta_strs)
    2.36 +     val _ = trace ("\nAxioms: " ^ onestr ax_strs)
    2.37 +     val _ = trace ("\nMeta_strs: " ^ onestr meta_strs)
    2.38  
    2.39       (* get list of axioms as thms with their variables *)
    2.40  
    2.41 @@ -283,25 +286,23 @@
    2.42  
    2.43  
    2.44  fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr = 
    2.45 - let val _ = File.append(File.tmp_path (Path.basic "prover_lemmastring"))
    2.46 -               ("proofstr is " ^ proofstr ^
    2.47 + let val _ = trace
    2.48 +               ("\nGetting lemma names. proofstr is " ^ proofstr ^
    2.49                  "\ngoalstr is " ^ goalstring ^
    2.50                  "\nnum of clauses is " ^ string_of_int (Array.length clause_arr))
    2.51       val axiom_names = getax proofstr clause_arr
    2.52       val ax_str = rules_to_string axiom_names
    2.53      in 
    2.54 -	 File.append(File.tmp_path (Path.basic "prover_lemmastring"))
    2.55 -	            ("\nlemma list is: " ^ ax_str);
    2.56 +	 trace ("\nDone. Lemma list is " ^ ax_str);
    2.57           TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
    2.58                    ax_str ^ "\n");
    2.59  	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
    2.60  	 TextIO.flushOut toParent;
    2.61 -
    2.62  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
    2.63      end
    2.64      handle exn => (*FIXME: exn handler is too general!*)
    2.65 -     (File.write(File.tmp_path (Path.basic "proverString_handler")) 
    2.66 -         ("In exception handler: " ^ Toplevel.exn_message exn);
    2.67 +     (trace ("\nprover_lemma_list_aux: In exception handler: " ^ 
    2.68 +             Toplevel.exn_message exn);
    2.69        TextIO.output (toParent, "Translation failed for the proof: " ^ 
    2.70                       remove_linebreaks proofstr ^ "\n");
    2.71        TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
    2.72 @@ -318,17 +319,13 @@
    2.73  (**** Full proof reconstruction for SPASS (not really working) ****)
    2.74  
    2.75  fun spass_reconstruct proofstr goalstring toParent ppid thms clause_arr = 
    2.76 -  let val _ = File.write(File.tmp_path (Path.basic "prover_reconstruction")) 
    2.77 -                 ("proofstr is: "^proofstr)
    2.78 +  let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr)
    2.79        val tokens = #1(lex proofstr)
    2.80  
    2.81 -  (***********************************)
    2.82    (* parse spass proof into datatype *)
    2.83    (***********************************)
    2.84        val proof_steps = parse tokens
    2.85 -
    2.86 -      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))
    2.87 -                      ("Did parsing on "^proofstr)
    2.88 +      val _ = trace "\nParsing finished"
    2.89      
    2.90    (************************************)
    2.91    (* recreate original subgoal as thm *)
    2.92 @@ -341,17 +338,15 @@
    2.93        val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr
    2.94        
    2.95        (*val numcls_string = numclstr ( vars, numcls) ""*)
    2.96 -      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) "got axioms"
    2.97 +      val _ = trace "\ngot axioms"
    2.98  	
    2.99    (************************************)
   2.100    (* translate proof                  *)
   2.101    (************************************)
   2.102 -      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))                                                                           
   2.103 -                       ("about to translate proof, steps: "
   2.104 -                       ^(init_proofsteps_to_string proof_steps ""))
   2.105 +      val _ = trace ("\nabout to translate proof, steps: "
   2.106 +                       ^ (init_proofsteps_to_string proof_steps ""))
   2.107        val (newthm,proof) = translate_proof numcls  proof_steps vars
   2.108 -      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))                                                                       
   2.109 -                       ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
   2.110 +      val _ = trace ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
   2.111    (***************************************************)
   2.112    (* transfer necessary steps as strings to Isabelle *)
   2.113    (***************************************************)
   2.114 @@ -368,9 +363,8 @@
   2.115                         else []
   2.116        val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
   2.117        val frees_str = "["^(thmvars_to_string frees "")^"]"
   2.118 -      val _ = File.write (File.tmp_path (Path.basic "reconstringfile"))
   2.119 -                          (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   2.120        val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   2.121 +      val _ = trace ("\nReconstruction:\n" ^ reconstr)
   2.122    in 
   2.123         TextIO.output (toParent, reconstr^"\n");
   2.124         TextIO.output (toParent, goalstring^"\n");
   2.125 @@ -379,8 +373,7 @@
   2.126         all_tac
   2.127    end
   2.128    handle exn => (*FIXME: exn handler is too general!*)
   2.129 -   (File.append(File.tmp_path (Path.basic "prover_reconstruction"))
   2.130 -       ("In exception handler: " ^ Toplevel.exn_message exn);
   2.131 +   (trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn);
   2.132      TextIO.output (toParent,"Translation failed for the proof:"^
   2.133           (remove_linebreaks proofstr) ^"\n");
   2.134      TextIO.output (toParent, goalstring^"\n");
   2.135 @@ -667,7 +660,7 @@
   2.136  		(isar_lines firststeps "")^
   2.137  		(last_isar_line laststep)^
   2.138  		("qed")
   2.139 -	val _ = File.write (File.tmp_path (Path.basic "isar_proof_file")) isar_proof
   2.140 +	val _ = trace ("\nto_isar_proof returns " ^ isar_proof)
   2.141      in
   2.142  	isar_proof
   2.143      end;
   2.144 @@ -684,8 +677,7 @@
   2.145  
   2.146  fun apply_res_thm str goalstring  = 
   2.147    let val tokens = #1 (lex str);
   2.148 -      val _ = File.append (File.tmp_path (Path.basic "apply_res_1")) 
   2.149 -	 ("str is: "^str^" goalstr is: "^goalstring^"\n")	
   2.150 +      val _ = trace ("\napply_res_thm. str is: "^str^" goalstr is: "^goalstring^"\n")	
   2.151        val (frees,recon_steps) = parse_step tokens 
   2.152    in 
   2.153        to_isar_proof (frees, recon_steps, goalstring)