# HG changeset patch
# User blanchet
# Date 1354924130 -3600
# Node ID 9762fe72936edd5172fa5536b132785d28785a40
# Parent  5291606b21e23fb4b57f0897a47247a090616bd0
store evaluation output in a file

diff -r 5291606b21e2 -r 9762fe72936e src/HOL/TPTP/MaSh_Eval.thy
--- a/src/HOL/TPTP/MaSh_Eval.thy	Sat Dec 08 00:48:50 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Sat Dec 08 00:48:50 2012 +0100
@@ -28,6 +28,7 @@
 ML {*
 if do_it then
   evaluate_mash_suggestions @{context} params "/tmp/mash_suggestions"
+      "/tmp/mash_eval.out"
 else
   ()
 *}
diff -r 5291606b21e2 -r 9762fe72936e src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Sat Dec 08 00:48:50 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Sat Dec 08 00:48:50 2012 +0100
@@ -9,7 +9,8 @@
 sig
   type params = Sledgehammer_Provers.params
 
-  val evaluate_mash_suggestions : Proof.context -> params -> string -> unit
+  val evaluate_mash_suggestions :
+    Proof.context -> params -> string -> string -> unit
 end;
 
 structure MaSh_Eval : MASH_EVAL =
@@ -25,14 +26,17 @@
 
 val all_names = map (rpair () o nickname_of) #> Symtab.make
 
-fun evaluate_mash_suggestions ctxt params file_name =
+fun evaluate_mash_suggestions ctxt params sugg_file_name out_file_name =
   let
+    val out_path = out_file_name |> Path.explode
+    val _ = File.write out_path ""
+    fun print s = (tracing s; File.append out_path (s ^ "\n"))
     val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
       Sledgehammer_Isar.default_params ctxt []
     val prover = hd provers
     val slack_max_facts = generous_max_facts (the max_facts)
-    val path = file_name |> Path.explode
-    val lines = path |> File.read_lines
+    val sugg_path = sugg_file_name |> Path.explode
+    val lines = sugg_path |> File.read_lines
     val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val facts = all_facts ctxt false Symtab.empty [] [] css
     val all_names = all_names (facts |> map snd)
@@ -103,7 +107,7 @@
       in
         ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
          isar_s]
-        |> cat_lines |> tracing
+        |> cat_lines |> print
       end
     fun total_of heading ok n =
       "  " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
@@ -117,15 +121,15 @@
        "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
     val n = length lines
   in
-    tracing " * * *";
-    tracing ("Options: " ^ commas options);
+    print " * * *";
+    print ("Options: " ^ commas options);
     List.app solve_goal (tag_list 1 lines);
     ["Successes (of " ^ string_of_int n ^ " goals)",
      total_of MePoN mepo_ok n,
      total_of MaShN mash_ok n,
      total_of MeshN mesh_ok n,
      total_of IsarN isar_ok n]
-    |> cat_lines |> tracing
+    |> cat_lines |> print
   end
 
 end;