--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Wed Jul 28 14:16:19 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Wed Jul 28 19:17: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);
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Wed Jul 28 14:16:19 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Wed Jul 28 19:17: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 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 ...]
@@ -148,7 +147,7 @@
-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
@@ -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 14:16:19 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Wed Jul 28 19:17: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 14:16:19 2021 +0200
+++ b/src/HOL/Tools/etc/options Wed Jul 28 19:17:31 2021 +0200
@@ -59,6 +59,9 @@
option mirabelle_max_calls : int = 0
-- "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)"