# HG changeset patch # User desharna # Date 1627492651 -7200 # Node ID a2cbe81e1e32e13e9d18d99d507ace31432834bd # Parent b93d8c2ebab08db8a055844bd316c3a985231c00 changed Mirabelle_Sledgehammer keep option from path to boolean diff -r b93d8c2ebab0 -r a2cbe81e1e32 src/HOL/Tools/Mirabelle/mirabelle.ML --- 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>\mirabelle_stride\; val mirabelle_max_calls = Options.default_int \<^system_option>\mirabelle_max_calls\; val mirabelle_theories = Options.default_string \<^system_option>\mirabelle_theories\; + val mirabelle_output_dir = Options.default_string \<^system_option>\mirabelle_output_dir\; 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); diff -r b93d8c2ebab0 -r a2cbe81e1e32 src/HOL/Tools/Mirabelle/mirabelle.scala --- 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() diff -r b93d8c2ebab0 -r a2cbe81e1e32 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- 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 => diff -r b93d8c2ebab0 -r a2cbe81e1e32 src/HOL/Tools/etc/options --- 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)"