# HG changeset patch
# User desharna
# Date 1627474579 -7200
# Node ID b93d8c2ebab08db8a055844bd316c3a985231c00
# Parent  97ad1687cec774b6dd4789371cd3b43a262daff6
added automatic uniform stride option to Mirabelle

diff -r 97ad1687cec7 -r b93d8c2ebab0 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Jul 28 10:21:02 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Jul 28 14:16:19 2021 +0200
@@ -1247,9 +1247,9 @@
     -A ACTION    add to list of actions
     -O DIR       output directory for log files (default: "mirabelle")
     -T THEORY    theory restriction: NAME or NAME[FIRST_LINE:LAST_LINE]
-    -m INT       max. no. of calls to each Mirabelle action (default 0)
-    -s INT       run actions on every nth goal (default 1)
-    -t SECONDS   timeout for each action (default 30.000)
+    -m INT       max. no. of calls to each action (0: unbounded) (default 0)
+    -s INT       run actions on every nth goal (0: uniform distribution) (default 1)
+    -t SECONDS   timeout in seconds for each action (default 30)
     ...
 
   Apply the given ACTIONs at all theories and proof steps of the
diff -r 97ad1687cec7 -r b93d8c2ebab0 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Wed Jul 28 10:21:02 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Wed Jul 28 14:16:19 2021 +0200
@@ -209,13 +209,22 @@
           loaded_theories
           |> map_index I
           |> maps make_commands
-          |> map_index I
-          |> maps (fn (n, command) =>
-            let val (m, k) = Integer.div_mod (n + 1) mirabelle_stride in
-              if k = 0 andalso (mirabelle_max_calls <= 0 orelse m <= mirabelle_max_calls) then
-                map (fn context => (context, command)) contexts
-              else
-                []
+          |> (fn xs => fold_map (fn x => fn i => ((i, x), i + 1)) xs 0)
+          |> (fn (indexed_commands, commands_length) =>
+            let
+              val stride =
+                if mirabelle_stride <= 0 then
+                  Integer.max 1 (commands_length div mirabelle_max_calls)
+                else
+                  mirabelle_stride
+            in
+              maps (fn (n, command) =>
+              let val (m, k) = Integer.div_mod (n + 1) stride in
+                if k = 0 andalso (mirabelle_max_calls <= 0 orelse m <= mirabelle_max_calls) then
+                  map (fn context => (context, command)) contexts
+                else
+                  []
+              end) indexed_commands
             end)
           |> Par_List.map (fn ((action, context), command) => apply_action action context command);
 
diff -r 97ad1687cec7 -r b93d8c2ebab0 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Wed Jul 28 10:21:02 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Wed Jul 28 14:16:19 2021 +0200
@@ -136,9 +136,9 @@
     var verbose = false
     var exclude_sessions: List[String] = Nil
 
-    val default_max_calls = options.int("mirabelle_max_calls")
-    val default_stride = options.int("mirabelle_stride")
-    val default_timeout = options.seconds("mirabelle_timeout")
+    val mirabelle_max_calls = options.check_name("mirabelle_max_calls")
+    val mirabelle_stride = options.check_name("mirabelle_stride")
+    val mirabelle_timeout = options.check_name("mirabelle_timeout")
 
     val getopts = Getopts("""
 Usage: isabelle mirabelle [OPTIONS] [SESSIONS ...]
@@ -155,10 +155,10 @@
     -d DIR       include session directory
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
-    -m INT       max. no. of calls to each Mirabelle action (default """ + default_max_calls + """)
+    -m INT       """ + mirabelle_max_calls.description + " (default " + mirabelle_max_calls.default_value + """)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
-    -s INT       run actions on every nth goal (default """ + default_stride + """)
-    -t SECONDS   timeout for each action (default """ + default_timeout + """)
+    -s INT       """ + mirabelle_stride.description + " (default " + mirabelle_stride.default_value + """)
+    -t SECONDS   """ + mirabelle_timeout.description + " (default " + mirabelle_timeout.default_value + """)
     -v           verbose
     -x NAME      exclude session NAME and all descendants
 
diff -r 97ad1687cec7 -r b93d8c2ebab0 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Wed Jul 28 10:21:02 2021 +0200
+++ b/src/HOL/Tools/etc/options	Wed Jul 28 14:16:19 2021 +0200
@@ -51,13 +51,13 @@
 section "Mirabelle"
 
 option mirabelle_timeout : real = 30
-  -- "default timeout for Mirabelle actions"
+  -- "timeout in seconds for each action"
 
 option mirabelle_stride : int = 1
-  -- "default stride for running Mirabelle actions on every nth goal"
+  -- "run actions on every nth goal (0: uniform distribution)"
 
 option mirabelle_max_calls : int = 0
-  -- "default max. no. of calls to each Mirabelle action (0: unbounded)"
+  -- "max. no. of calls to each action (0: unbounded)"
 
 option mirabelle_actions : string = ""
   -- "Mirabelle actions (outer syntax, separated by semicolons)"