--- 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
--- 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);
--- 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
--- 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)"