# HG changeset patch
# User desharna
# Date 1639731097 -3600
# Node ID 15ce207f69c8e7f3aaf5411bec41d0b092a1c3f5
# Parent  0dd14d8b16da51396b68ce0c7e8336c9f4bdddf7
added support for initialization messages to Mirabelle

diff -r 0dd14d8b16da -r 15ce207f69c8 src/HOL/Mirabelle.thy
--- a/src/HOL/Mirabelle.thy	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Mirabelle.thy	Fri Dec 17 09:51:37 2021 +0100
@@ -13,7 +13,7 @@
 
 ML \<open>
 signature MIRABELLE_ACTION = sig
-  val make_action : Mirabelle.action_context -> Mirabelle.action
+  val make_action : Mirabelle.action_context -> string * Mirabelle.action
 end
 \<close>
 
diff -r 0dd14d8b16da -r 15ce207f69c8 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Fri Dec 17 09:51:37 2021 +0100
@@ -14,7 +14,7 @@
   type command =
     {theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}
   type action = {run_action: command -> string, finalize: unit -> string}
-  val register_action: string -> (action_context -> action) -> unit
+  val register_action: string -> (action_context -> string * action) -> unit
 
   (*utility functions*)
   val print_exn: exn -> string
@@ -71,7 +71,7 @@
 
 local
   val actions = Synchronized.var "Mirabelle.actions"
-    (Symtab.empty : (action_context -> action) Symtab.table);
+    (Symtab.empty : (action_context -> string * action) Symtab.table);
 in
 
 fun register_action name make_action =
@@ -100,6 +100,21 @@
 fun make_action_path ({index, label, name, ...} : action_context) =
   Path.basic (if label = "" then string_of_int index ^ "." ^ name else label);
 
+fun initialize_action (make_action : action_context -> string * action) context =
+  let
+    val (s, action) = make_action context
+    val action_path = make_action_path context;
+    val export_name =
+      Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "initialize");
+    val () =
+      if s <> "" then
+        Export.export \<^theory> export_name [XML.Text s]
+      else
+        ()
+  in
+    action
+  end
+
 fun finalize_action ({finalize, ...} : action) context =
   let
     val s = run_action_function finalize;
@@ -232,7 +247,7 @@
                 {index = n, label = label, name = name, arguments = args,
                  timeout = mirabelle_timeout, output_dir = output_dir};
             in
-              (make_action context, context)
+              (initialize_action make_action context, context)
             end);
         in
           (* run actions on all relevant goals *)
diff -r 0dd14d8b16da -r 15ce207f69c8 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Dec 17 09:51:37 2021 +0100
@@ -85,7 +85,8 @@
                   val lines = Pretty.string_of(yxml).trim()
                   val prefix =
                     Export.explode_name(args.name) match {
-                      case List("mirabelle", action, "finalize") => action + " finalize  "
+                      case List("mirabelle", action, "initialize") => action + " initialize "
+                      case List("mirabelle", action, "finalize") => action + " finalize   "
                       case List("mirabelle", action, "goal", goal_name, line, offset) =>
                         action + " goal." + String.format("%-5s", goal_name) + " " + args.theory_name + " " +
                           line + ":" + offset + "  "
diff -r 0dd14d8b16da -r 15ce207f69c8 src/HOL/Tools/Mirabelle/mirabelle_arith.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML	Fri Dec 17 09:51:37 2021 +0100
@@ -16,7 +16,7 @@
       (case Timing.timing (Mirabelle.can_apply timeout Arith_Data.arith_tac) pre of
         ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
       | (_, false) => "failed")
-  in {run_action = run_action, finalize = K ""} end
+  in ("", {run_action = run_action, finalize = K ""}) end
 
 val () = Mirabelle.register_action "arith" make_action
 
diff -r 0dd14d8b16da -r 15ce207f69c8 src/HOL/Tools/Mirabelle/mirabelle_metis.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_metis.ML	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML	Fri Dec 17 09:51:37 2021 +0100
@@ -21,7 +21,7 @@
         (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
         |> not (null names) ? suffix (":\n" ^ commas names)
       end
-  in {run_action = run_action, finalize = K ""} end
+  in ("", {run_action = run_action, finalize = K ""}) end
 
 val () = Mirabelle.register_action "metis" make_action
 
diff -r 0dd14d8b16da -r 15ce207f69c8 src/HOL/Tools/Mirabelle/mirabelle_presburger.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML	Fri Dec 17 09:51:37 2021 +0100
@@ -14,7 +14,7 @@
       (case Timing.timing (Mirabelle.can_apply timeout (Cooper.tac true [] [])) pre of
         ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
       | (_, false) => "failed")
-  in {run_action = run_action, finalize = K ""} end
+  in ("", {run_action = run_action, finalize = K ""}) end
 
 val () = Mirabelle.register_action "presburger" make_action
 
diff -r 0dd14d8b16da -r 15ce207f69c8 src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML	Fri Dec 17 09:51:37 2021 +0100
@@ -19,7 +19,7 @@
       (case Timeout.apply timeout quickcheck pre of
         NONE => "no counterexample"
       | SOME _ => "counterexample found")
-  in {run_action = run_action, finalize = K ""} end
+  in ("", {run_action = run_action, finalize = K ""}) end
 
 val () = Mirabelle.register_action "quickcheck" make_action
 
diff -r 0dd14d8b16da -r 15ce207f69c8 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Dec 17 09:51:37 2021 +0100
@@ -536,6 +536,8 @@
     val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data
     val change_data = Synchronized.change data
 
+    val init_msg = "Params for sledgehammer: " ^ Sledgehammer_Prover.string_of_params params
+
     fun run_action ({theory_index, name, pos, pre, ...} : Mirabelle.command) =
       let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
         if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then
@@ -561,7 +563,7 @@
       end
 
     fun finalize () = log_data (Synchronized.value data)
-  in {run_action = run_action, finalize = finalize} end
+  in (init_msg, {run_action = run_action, finalize = finalize}) end
 
 val () = Mirabelle.register_action "sledgehammer" make_action
 
diff -r 0dd14d8b16da -r 15ce207f69c8 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML	Fri Dec 17 09:51:37 2021 +0100
@@ -179,7 +179,7 @@
             (Synchronized.value num_lost_facts) ^ "%"
       else
         ""
-  in {run_action = run_action, finalize = finalize} end
+  in ("", {run_action = run_action, finalize = finalize}) end
 
 val () = Mirabelle.register_action "sledgehammer_filter" make_action
 
diff -r 0dd14d8b16da -r 15ce207f69c8 src/HOL/Tools/Mirabelle/mirabelle_try0.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML	Fri Dec 17 09:51:37 2021 +0100
@@ -18,7 +18,7 @@
         "succeeded"
       else
         ""
-  in {run_action = run_action, finalize = K ""} end
+  in ("", {run_action = run_action, finalize = K ""}) end
 
 val () = Mirabelle.register_action "try0" make_action
 
diff -r 0dd14d8b16da -r 15ce207f69c8 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Dec 17 09:51:37 2021 +0100
@@ -47,6 +47,7 @@
      preplay_timeout : Time.time,
      expect : string}
 
+  val string_of_params : params -> string
   val set_params_provers : params -> string list -> params
 
   type prover_problem =
@@ -143,6 +144,9 @@
    preplay_timeout : Time.time,
    expect : string}
 
+fun string_of_params (params : params) =
+  YXML.content_of (ML_Pretty.string_of_polyml (ML_system_pretty (params, 100)))
+
 fun set_params_provers params provers =
   {debug = #debug params,
    verbose = #verbose params,