# HG changeset patch
# User desharna
# Date 1623396823 -7200
# Node ID 4eac16052a944660cdceaa75bdc320318d4abf73
# Parent  77306bf4e1eec88b4da6e47363299764b538ef39
tuned Mirabelle

diff -r 77306bf4e1ee -r 4eac16052a94 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Thu Jun 10 11:54:14 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Fri Jun 11 09:33:43 2021 +0200
@@ -151,12 +151,7 @@
 val _ =
   Build.add_hook (fn qualifier => fn loaded_theories =>
     let
-      val mirabelle_timeout = Options.default_seconds \<^system_option>\<open>mirabelle_timeout\<close>;
-      val mirabelle_stride = Options.default_int \<^system_option>\<open>mirabelle_stride\<close>;
-      val mirabelle_max_calls = Options.default_int \<^system_option>\<open>mirabelle_max_calls\<close>;
       val mirabelle_actions = Options.default_string \<^system_option>\<open>mirabelle_actions\<close>;
-      val mirabelle_theories = Options.default_string \<^system_option>\<open>mirabelle_theories\<close>;
-
       val actions =
         (case read_actions mirabelle_actions of
           SOME actions => actions
@@ -166,6 +161,10 @@
         ()
       else
         let
+          val mirabelle_timeout = Options.default_seconds \<^system_option>\<open>mirabelle_timeout\<close>;
+          val mirabelle_stride = Options.default_int \<^system_option>\<open>mirabelle_stride\<close>;
+          val mirabelle_max_calls = Options.default_int \<^system_option>\<open>mirabelle_max_calls\<close>;
+          val mirabelle_theories = Options.default_string \<^system_option>\<open>mirabelle_theories\<close>;
           val check_theory = check_theories (space_explode "," mirabelle_theories);
 
           fun make_commands (thy_index, (thy, segments)) =
@@ -212,8 +211,7 @@
               else
                 []
             end)
-          |> Par_List.map (fn ((action, context), command) => apply_action action context command)
-          |> ignore;
+          |> Par_List.map (fn ((action, context), command) => apply_action action context command);
 
           (* finalize actions *)
           List.app (uncurry finalize_action) contexts
diff -r 77306bf4e1ee -r 4eac16052a94 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Jun 10 11:54:14 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Jun 11 09:33:43 2021 +0200
@@ -86,9 +86,9 @@
                     for (export <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) {
                       val prefix = args.name.split('/') match {
                         case Array("mirabelle", action, "finalize") =>
-                          s"${action} finalize "
+                          s"${action} finalize  "
                         case Array("mirabelle", action, "goal", goal_name, line, offset) =>
-                          s"${action} goal.${goal_name} ${args.theory_name} ${line}:${offset} "
+                          s"${action} goal.${goal_name} ${args.theory_name} ${line}:${offset}  "
                         case _ => ""
                       }
                       val lines = Pretty.string_of(export.uncompressed_yxml).trim()
@@ -162,7 +162,7 @@
     -v           verbose
     -x NAME      exclude session NAME and all descendants
 
-  Apply the given actions at all theories and proof steps of the
+  Apply the given ACTIONs at all theories and proof steps of the
   specified sessions.
 
   The absence of theory restrictions (option -T) means to check all
diff -r 77306bf4e1ee -r 4eac16052a94 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Thu Jun 10 11:54:14 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Jun 11 09:33:43 2021 +0200
@@ -32,7 +32,7 @@
 val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*)
 val minimizeK = "minimize" (*=BOOL: instruct sledgehammer to run its minimizer*)
 val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*)
-val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (ie. using metis/smt)*)
+val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (e.g. using metis)*)
 val proverK = "prover" (*=STRING: name of the external prover to call*)
 val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*)
 val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*)