--- a/src/Doc/Sledgehammer/document/root.tex Wed Jul 28 17:30:18 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Jul 30 16:21:31 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
@@ -1330,16 +1330,16 @@
\begin{verbatim}
isabelle mirabelle -d $AFP -O output \
- -A "sledgehammer[prover=e, prover_timeout=5, keep=/tptp]" \
+ -A "sledgehammer[prover=e, prover_timeout=5, keep=true]" \
VeriComp
\end{verbatim}
This command generates TPTP files using Sledgehammer. Since the file
is generated at the very beginning of every Sledgehammer invocation,
a timeout of five seconds making the prover fail faster speeds up
-processing the subgoals. The results are written in the specified directory
-(\texttt{/tptp}), which must exist beforehand. A TPTP file is generated
-for each subgoal.
+processing the subgoals. The results are written in an action-specific
+subdirectory of the specified output directory (\texttt{output}). A TPTP
+file is generated for each subgoal.
\let\em=\sl
\bibliography{manual}{}
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Wed Jul 28 17:30:18 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Fri Jul 30 16:21:31 2021 +0200
@@ -8,7 +8,8 @@
signature MIRABELLE =
sig
(*core*)
- type action_context = {index: int, name: string, arguments: Properties.T, timeout: Time.time}
+ type action_context =
+ {index: int, name: string, arguments: Properties.T, timeout: Time.time, output_dir: Path.T}
type command =
{theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}
type action = {run_action: command -> string, finalize: unit -> string}
@@ -45,7 +46,8 @@
type command =
{theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state};
-type action_context = {index: int, name: string, arguments: Properties.T, timeout: Time.time};
+type action_context =
+ {index: int, name: string, arguments: Properties.T, timeout: Time.time, output_dir: Path.T};
type action = {run_action: command -> string, finalize: unit -> string};
local
@@ -171,6 +173,7 @@
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 mirabelle_output_dir = Options.default_string \<^system_option>\<open>mirabelle_output_dir\<close>;
val check_theory = check_theories (space_explode "," mirabelle_theories);
fun make_commands (thy_index, (thy, segments)) =
@@ -200,7 +203,12 @@
val contexts = actions |> map_index (fn (n, (name, args)) =>
let
val make_action = the (get_action name);
- val context = {index = n, name = name, arguments = args, timeout = mirabelle_timeout};
+ val action_subdir = string_of_int n ^ "." ^ name
+ val output_dir =
+ Path.append (Path.explode mirabelle_output_dir) (Path.basic action_subdir)
+ val context =
+ {index = n, name = name, arguments = args, timeout = mirabelle_timeout,
+ output_dir = output_dir};
in
(make_action context, context)
end);
@@ -209,13 +217,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 17:30:18 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Fri Jul 30 16:21:31 2021 +0200
@@ -114,32 +114,31 @@
/* Isabelle tool wrapper */
- val default_output_dir: Path = Path.explode("mirabelle")
-
val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools",
Scala_Project.here, args =>
{
val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
+ var options = Options.init(opts = build_options)
+ 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 mirabelle_output_dir = options.check_name("mirabelle_output_dir")
+
var actions: List[String] = Nil
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
var numa_shuffling = false
- var output_dir = default_output_dir
+ var output_dir = Path.explode(mirabelle_output_dir.default_value)
var theories: List[String] = Nil
var exclude_session_groups: List[String] = Nil
var all_sessions = false
var dirs: List[Path] = Nil
var session_groups: List[String] = Nil
var max_jobs = 1
- var options = Options.init(opts = build_options)
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 getopts = Getopts("""
Usage: isabelle mirabelle [OPTIONS] [SESSIONS ...]
@@ -148,17 +147,17 @@
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-N cyclic shuffling of NUMA CPU nodes (performance tuning)
- -O DIR output directory for log files (default: """ + default_output_dir + """)
+ -O DIR """ + mirabelle_output_dir.description + " (default: " + mirabelle_output_dir.default_value + """)
-T THEORY theory restriction: NAME or NAME[FIRST_LINE:LAST_LINE]
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-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
@@ -193,6 +192,8 @@
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+ options = options + ("mirabelle_output_dir=" + output_dir.implode)
+
val sessions = getopts(args)
if (actions.isEmpty) getopts.usage()
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Wed Jul 28 17:30:18 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Jul 30 16:21:31 2021 +0200
@@ -24,7 +24,7 @@
val fact_filterK = "fact_filter" (*=STRING: fact filter*)
val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*)
val isar_proofsK = "isar_proofs" (*=SMART_BOOL: enable Isar proof generation*)
-val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*)
+val keepK = "keep" (*=BOOL: keep temporary files created by sledgehammer*)
val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*)
val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*)
val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*)
@@ -53,6 +53,7 @@
val max_facts_default = "smart"
val slice_default = "true"
val check_trivial_default = false
+val keep_default = false
(*If a key is present in args then augment a list with its pair*)
(*This is used to avoid fixing default values at the Mirabelle level, and
@@ -428,7 +429,7 @@
in
-fun run_sledgehammer change_data thy_index trivial args proof_method named_thms pos st =
+fun run_sledgehammer change_data thy_index trivial output_dir args proof_method named_thms pos st =
let
val thy = Proof.theory_of st
val thy_name = Context.theory_name thy
@@ -453,13 +454,16 @@
val term_order = AList.lookup (op =) args term_orderK
val force_sos = AList.lookup (op =) args force_sosK
|> Option.map (curry (op <>) "false")
- val dir = AList.lookup (op =) args keepK
- |> Option.map (fn dir =>
+ val keep_dir =
+ if Mirabelle.get_bool_argument args (keepK, keep_default) then
let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in
- Path.append (Path.explode dir) (Path.basic subdir)
+ Path.append output_dir (Path.basic subdir)
|> Isabelle_System.make_directory
|> Path.implode
- end)
+ |> SOME
+ end
+ else
+ NONE
val timeout = Mirabelle.get_int_argument args (prover_timeoutK, 30)
(* always use a hard timeout, but give some slack so that the automatic
minimizer has a chance to do its magic *)
@@ -476,7 +480,7 @@
run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans
uncurried_aliases e_selection_heuristic term_order force_sos
hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST
- minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st
+ minimizeLST max_new_mono_instancesLST max_mono_itersLST keep_dir pos st
in
(case result of
SH_OK (time_isa, time_prover, names) =>
@@ -584,7 +588,7 @@
val try_timeout = seconds 5.0
-fun make_action ({arguments, timeout, ...} : Mirabelle.action_context) =
+fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) =
let
val check_trivial =
Mirabelle.get_bool_argument arguments (check_trivialK, check_trivial_default)
@@ -605,7 +609,8 @@
check_trivial andalso Try0.try0 (SOME try_timeout) ([], [], [], []) pre
handle Timeout.TIMEOUT _ => false
val log1 =
- run_sledgehammer change_data theory_index trivial arguments meth named_thms pos pre
+ run_sledgehammer change_data theory_index trivial output_dir arguments meth named_thms
+ pos pre
val log2 =
(case !named_thms of
SOME thms =>
--- a/src/HOL/Tools/etc/options Wed Jul 28 17:30:18 2021 +0200
+++ b/src/HOL/Tools/etc/options Fri Jul 30 16:21:31 2021 +0200
@@ -51,13 +51,16 @@
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_output_dir : string = "mirabelle"
+ -- "output directory for log files and generated artefacts"
option mirabelle_actions : string = ""
-- "Mirabelle actions (outer syntax, separated by semicolons)"