# HG changeset patch
# User desharna
# Date 1695994063 -7200
# Node ID e4b4141e6954f15230f21057c461ed89c7502db9
# Parent  eace130baedcf5eb782dfad23368191566f8744c
added parallel_group_size option to Mirabelle

diff -r eace130baedc -r e4b4141e6954 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Sun Feb 04 23:05:35 2024 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Fri Sep 29 15:27:43 2023 +0200
@@ -207,8 +207,13 @@
           val mirabelle_randomize = Options.default_int \<^system_option>\<open>mirabelle_randomize\<close>;
           val mirabelle_theories = Options.default_string \<^system_option>\<open>mirabelle_theories\<close>;
           val mirabelle_output_dir = Options.default_string \<^system_option>\<open>mirabelle_output_dir\<close>;
+          val mirabelle_parallel_group_size = Options.default_int \<^system_option>\<open>mirabelle_parallel_group_size\<close>;
           val check_theory = check_theories (space_explode "," mirabelle_theories);
 
+          fun parallel_app (f : 'a -> unit) (xs : 'a list) : unit =
+            chop_groups mirabelle_parallel_group_size xs
+            |> List.app (ignore o Par_List.map f)
+
           fun make_commands (thy_index, (thy, segments)) =
             let
               val thy_long_name = Context.theory_long_name thy;
@@ -275,7 +280,7 @@
               end) indexed_commands
             end)
           (* 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) =>
+          |> (if mirabelle_dry_run then List.app else parallel_app) (fn ((action, context), command) =>
               apply_action (if mirabelle_dry_run then dry_run_action else action) context command);
 
           (* finalize actions *)
diff -r eace130baedc -r e4b4141e6954 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Sun Feb 04 23:05:35 2024 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Sep 29 15:27:43 2023 +0200
@@ -112,6 +112,7 @@
       val mirabelle_stride = options.check_name("mirabelle_stride")
       val mirabelle_timeout = options.check_name("mirabelle_timeout")
       val mirabelle_output_dir = options.check_name("mirabelle_output_dir")
+      val mirabelle_parallel_group_size = options.check_name("mirabelle_parallel_group_size")
 
       var actions: List[String] = Nil
       var base_sessions: List[String] = Nil
@@ -144,6 +145,7 @@
     -j INT       maximum number of parallel jobs (default 1)
     -m INT       """ + mirabelle_max_calls.description + " (default " + mirabelle_max_calls.default_value + """)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -p INT       """ + mirabelle_parallel_group_size.description + " (default " + mirabelle_parallel_group_size.default_value + """)
     -r INT       """ + mirabelle_randomize.description + " (default " + mirabelle_randomize.default_value + """)
     -s INT       """ + mirabelle_stride.description + " (default " + mirabelle_stride.default_value + """)
     -t SECONDS   """ + mirabelle_timeout.description + " (default " + mirabelle_timeout.default_value + """)
@@ -177,6 +179,7 @@
         "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
         "m:" -> (arg => options = options + ("mirabelle_max_calls=" + arg)),
         "o:" -> (arg => options = options + arg),
+        "p:" -> (arg => options = options + ("mirabelle_parallel_group_size=" + arg)),
         "r:" -> (arg => options = options + ("mirabelle_randomize=" + arg)),
         "s:" -> (arg => options = options + ("mirabelle_stride=" + arg)),
         "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)),
diff -r eace130baedc -r e4b4141e6954 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Sun Feb 04 23:05:35 2024 +0100
+++ b/src/HOL/Tools/etc/options	Fri Sep 29 15:27:43 2023 +0200
@@ -65,6 +65,9 @@
 option mirabelle_output_dir : string = "mirabelle"
   -- "output directory for log files and generated artefacts"
 
+option mirabelle_parallel_group_size : int = 0
+  -- "number of actions to perform in parallel (0: unbounded)"
+
 option mirabelle_actions : string = ""
   -- "Mirabelle actions (outer syntax, separated by semicolons)"