src/HOL/TPTP/mash_eval.ML

 
 signature MASH_EVAL =
 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 =
 struct
 

 val MeshN = "Mesh"
 val IsarN = "Isar"
 
 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)
     val mepo_ok = Unsynchronized.ref 0
     val mash_ok = Unsynchronized.ref 0

            fn () => prove isar_ok IsarN fst isar_facts]
           |> Par_List.map (fn f => f ())
       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) ^ " (" ^
       Real.fmt (StringCvt.FIX (SOME 1))
                (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"

        "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
        the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
        "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;