# HG changeset patch
# User desharna
# Date 1642683329 -3600
# Node ID 003f378b78a5139d986ab2e0bf44a280e09f661c
# Parent  9fcf09cf7b36e824d2d78bb795a99755100aa6a3
added Mirabelle option "-y" for dry run

diff -r 9fcf09cf7b36 -r 003f378b78a5 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Thu Jan 20 13:53:13 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Thu Jan 20 13:55:29 2022 +0100
@@ -69,6 +69,8 @@
    output_dir: Path.T};
 type action = {run_action: command -> string, finalize: unit -> string};
 
+val dry_run_action : action = {run_action = K "", finalize = K ""}
+
 local
   val actions = Synchronized.var "Mirabelle.actions"
     (Symtab.empty : (action_context -> string * action) Symtab.table);
@@ -140,10 +142,7 @@
       Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path +
         line_path + offset_path + Path.basic (string_of_int (Time.toMilliseconds cpu)));
   in
-    if s <> "" then
-      Export.export thy export_name [XML.Text s]
-    else
-      ()
+    Export.export thy export_name [XML.Text s]
   end;
 
 
@@ -203,6 +202,7 @@
         ()
       else
         let
+          val mirabelle_dry_run = Options.default_bool \<^system_option>\<open>mirabelle_dry_run\<close>;
           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>;
@@ -276,7 +276,9 @@
                   []
               end) indexed_commands
             end)
-          |> Par_List.map (fn ((action, context), command) => apply_action action context command);
+          (* Don't use multithreading for a dry run because of the high per-thread overhead. *)
+          |> (if mirabelle_dry_run then map else Par_List.map) (fn ((action, context), command) =>
+              apply_action (if mirabelle_dry_run then dry_run_action else action) context command);
 
           (* finalize actions *)
           List.app (uncurry finalize_action) contexts
diff -r 9fcf09cf7b36 -r 003f378b78a5 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Jan 20 13:53:13 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Jan 20 13:55:29 2022 +0100
@@ -92,7 +92,7 @@
                           args.theory_name + " " + line + ":" + offset + "  "
                       case _ => ""
                     }
-                  val body = Library.prefix_lines(prefix, lines) + "\n"
+                  val body = (if (lines == "") prefix else Library.prefix_lines(prefix, lines)) + "\n"
                   val log_file = output_dir + Path.basic("mirabelle.log")
                   File.append(log_file, body)
                 case _ =>
@@ -118,6 +118,7 @@
     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 
     var options = Options.init(opts = build_options)
+    val mirabelle_dry_run = options.check_name("mirabelle_dry_run")
     val mirabelle_max_calls = options.check_name("mirabelle_max_calls")
     val mirabelle_randomize = options.check_name("mirabelle_randomize")
     val mirabelle_stride = options.check_name("mirabelle_stride")
@@ -160,6 +161,7 @@
     -t SECONDS   """ + mirabelle_timeout.description + " (default " + mirabelle_timeout.default_value + """)
     -v           verbose
     -x NAME      exclude session NAME and all descendants
+    -y           """ + mirabelle_dry_run.description + " (default " + mirabelle_dry_run.default_value + """)
 
   Apply the given ACTIONs at all theories and proof steps of the
   specified sessions.
@@ -191,7 +193,8 @@
       "s:" -> (arg => options = options + ("mirabelle_stride=" + arg)),
       "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)),
       "v" -> (_ => verbose = true),
-      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)),
+      "y" -> (arg => options = options + ("mirabelle_dry_run=true")))
 
     val sessions = getopts(args)
     if (actions.isEmpty) getopts.usage()
diff -r 9fcf09cf7b36 -r 003f378b78a5 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Thu Jan 20 13:53:13 2022 +0100
+++ b/src/HOL/Tools/etc/options	Thu Jan 20 13:55:29 2022 +0100
@@ -47,6 +47,9 @@
 
 section "Mirabelle"
 
+option mirabelle_dry_run : bool = false
+  -- "initialize the actions, print on which goals they would be run, and finalize the actions"
+
 option mirabelle_timeout : real = 30
   -- "timeout in seconds for each action"