--- 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>
--- 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 *)
--- 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 + " "
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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,