# HG changeset patch # User desharna # Date 1623316917 -7200 # Node ID 58f6b41efe8816b4ad0c0a9a6e027e67c33f1a69 # Parent c10fe904ac103eb2c638b50488b6072861321f94 refactored Mirabelle to produce output in real time diff -r c10fe904ac10 -r 58f6b41efe88 src/HOL/Mirabelle.thy --- a/src/HOL/Mirabelle.thy Sun Jun 06 21:39:26 2021 +0200 +++ b/src/HOL/Mirabelle.thy Thu Jun 10 11:21:57 2021 +0200 @@ -1,6 +1,8 @@ (* Title: HOL/Mirabelle.thy - Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Jasmin Blanchette, TU Munich + Author: Sascha Boehme, TU Munich Author: Makarius + Author: Martin Desharnais, UniBw Munich *) theory Mirabelle @@ -8,6 +10,13 @@ begin ML_file \Tools/Mirabelle/mirabelle.ML\ + +ML \ +signature MIRABELLE_ACTION = sig + val make_action : Mirabelle.action_context -> Mirabelle.action +end +\ + ML_file \Tools/Mirabelle/mirabelle_arith.ML\ ML_file \Tools/Mirabelle/mirabelle_metis.ML\ ML_file \Tools/Mirabelle/mirabelle_quickcheck.ML\ @@ -15,4 +24,4 @@ ML_file \Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\ ML_file \Tools/Mirabelle/mirabelle_try0.ML\ -end +end \ No newline at end of file diff -r c10fe904ac10 -r 58f6b41efe88 src/HOL/Tools/Mirabelle/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Jun 06 21:39:26 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Thu Jun 10 11:21:57 2021 +0200 @@ -1,23 +1,21 @@ (* Title: HOL/Mirabelle/Tools/mirabelle.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Jasmin Blanchette, TU Munich + Author: Sascha Boehme, TU Munich Author: Makarius + Author: Martin Desharnais, UniBw Munich *) signature MIRABELLE = sig (*core*) - val print_name: string -> string - val print_properties: Properties.T -> string - type context = - {index: int, tag: string, arguments: Properties.T, timeout: Time.time, theory: theory} - type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state} - val theory_action: binding -> (context -> command list -> XML.body) -> theory -> theory - val log_command: command -> XML.body -> XML.tree - val log_report: Properties.T -> XML.body -> XML.tree - val print_exn: exn -> string - val command_action: binding -> (context -> command -> string) -> theory -> theory + type action_context = {index: int, name: string, arguments: Properties.T, timeout: Time.time} + 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} + val register_action: string -> (action_context -> action) -> unit (*utility functions*) + val print_exn: exn -> string val can_apply : Time.time -> (Proof.context -> int -> tactic) -> Proof.state -> bool val theorems_in_proof_term : theory -> thm -> thm list @@ -37,9 +35,6 @@ val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords \<^theory>); -val print_name = Token.print_name keywords; -val print_properties = Token.print_properties keywords; - fun read_actions str = Token.read_body keywords (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params)) @@ -48,68 +43,69 @@ (* actions *) -type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}; -type context = - {index: int, tag: string, arguments: Properties.T, timeout: Time.time, theory: theory}; - -structure Data = Theory_Data -( - type T = (context -> command list -> XML.body) Name_Space.table; - val empty = Name_Space.empty_table "mirabelle_action"; - val extend = I; - val merge = Name_Space.merge_tables; -); +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 = {run_action: command -> string, finalize: unit -> string}; -fun theory_action binding action thy = - let val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming); - in thy |> Data.map (#2 o Name_Space.define context true (binding, action)) end; - - -(* log content *) +local + val actions = Synchronized.var "Mirabelle.actions" + (Symtab.empty : (action_context -> action) Symtab.table); +in -fun log_action name arguments = - XML.Elem (("action", (Markup.nameN, name) :: arguments), - [XML.Text (print_name name ^ (if null arguments then "" else " " ^ print_properties arguments))]); +val register_action = Synchronized.change actions oo curry Symtab.update; -fun log_command ({name, pos, ...}: command) body = - XML.Elem (("command", (Markup.nameN, name) :: Position.properties_of pos), body); +fun get_action name = Symtab.lookup (Synchronized.value actions) name; -fun log_report props body = - XML.Elem (("report", props), body); +end (* apply actions *) -fun apply_action index name arguments timeout commands thy = - let - val action = #2 (Name_Space.check (Context.Theory thy) (Data.get thy) (name, Position.none)); - val tag = "#" ^ Value.print_int index ^ " " ^ name ^ ": "; - val context = {index = index, tag = tag, arguments = arguments, timeout = timeout, theory = thy}; - val export_body = action context commands; - val export_head = log_action name arguments; - val export_name = Path.binding0 (Path.basic "mirabelle" + Path.basic (Value.print_int index)); - in - if null export_body then () - else Export.export thy export_name (export_head :: export_body) - end; - fun print_exn exn = (case exn of Timeout.TIMEOUT _ => "timeout" | ERROR msg => "error: " ^ msg - | exn => "exception:\n" ^ General.exnMessage exn); + | exn => "exception: " ^ General.exnMessage exn); -fun command_action binding action = +fun run_action_function f = + f () handle exn => + if Exn.is_interrupt exn then Exn.reraise exn + else print_exn exn; + +fun make_action_path (context as {index, name, ...} : action_context) = + Path.basic (string_of_int index ^ "." ^ name); + +fun finalize_action ({finalize, ...} : action) context = let - fun apply context command = - let val s = - action context command handle exn => - if Exn.is_interrupt exn then Exn.reraise exn - else #tag context ^ print_exn exn; - in - if s = "" then NONE - else SOME (log_command command [XML.Text s]) end; - in theory_action binding (map_filter o apply) end; + val s = run_action_function finalize; + val action_path = make_action_path context; + val export_name = + Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "finalize"); + in + if s <> "" then + Export.export \<^theory> export_name [XML.Text s] + else + () + end + +fun apply_action ({run_action, ...} : action) context (command as {pos, pre, ...} : command) = + let + val thy = Proof.theory_of pre; + val action_path = make_action_path context; + val goal_name_path = Path.basic (#name command) + val line_path = Path.basic (string_of_int (the (Position.line_of pos))); + val offset_path = Path.basic (string_of_int (the (Position.offset_of pos))); + val export_name = + Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path + + line_path + offset_path); + val s = run_action_function (fn () => run_action command); + in + if s <> "" then + Export.export thy export_name [XML.Text s] + else + () + end; (* theory line range *) @@ -147,9 +143,6 @@ fun check_pos range = check_line range o Position.line_of; in check_pos o get_theory end; -fun check_session qualifier thy_name (_: Position.T) = - Resources.theory_qualifier thy_name = qualifier; - (* presentation hook *) @@ -160,6 +153,7 @@ let val mirabelle_timeout = Options.default_seconds \<^system_option>\mirabelle_timeout\; val mirabelle_stride = Options.default_int \<^system_option>\mirabelle_stride\; + val mirabelle_max_calls = Options.default_int \<^system_option>\mirabelle_max_calls\; val mirabelle_actions = Options.default_string \<^system_option>\mirabelle_actions\; val mirabelle_theories = Options.default_string \<^system_option>\mirabelle_theories\; @@ -167,35 +161,62 @@ (case read_actions mirabelle_actions of SOME actions => actions | NONE => error ("Failed to parse mirabelle_actions: " ^ quote mirabelle_actions)); - val check = - if mirabelle_theories = "" then check_session qualifier - else check_theories (space_explode "," mirabelle_theories); + in + if null actions then + () + else + let + val check_theory = check_theories (space_explode "," mirabelle_theories); - fun theory_commands (thy, segments) = - let - val commands = segments - |> map_index (fn (n, {command = tr, prev_state = st, state = st', ...}) => - if n mod mirabelle_stride = 0 then + fun make_commands (thy_index, (thy, segments)) = + let + val thy_long_name = Context.theory_long_name thy; + val check_thy = check_theory thy_long_name; + fun make_command {command = tr, prev_state = st, state = st', ...} = let val name = Toplevel.name_of tr; val pos = Toplevel.pos_of tr; in if can (Proof.assert_backward o Toplevel.proof_of) st andalso - member (op =) whitelist name andalso - check (Context.theory_long_name thy) pos - then SOME {name = name, pos = pos, pre = Toplevel.proof_of st, post = st'} + member (op =) whitelist name andalso check_thy pos + then SOME {theory_index = thy_index, name = name, pos = pos, + pre = Toplevel.proof_of st, post = st'} else NONE - end - else NONE) - |> map_filter I; - in if null commands then NONE else SOME (thy, commands) end; + end; + in + if Resources.theory_qualifier thy_long_name = qualifier then + map_filter make_command segments + else + [] + end; - fun app_actions (thy, commands) = - (actions, ()) |-> fold_index (fn (index, (name, arguments)) => fn () => - apply_action (index + 1) name arguments mirabelle_timeout commands thy); - in - if null actions then () - else List.app app_actions (map_filter theory_commands loaded_theories) + (* initialize actions *) + 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}; + in + (make_action context, context) + end); + in + (* run actions on all relevant goals *) + 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 m <= mirabelle_max_calls then + map (fn context => (context, command)) contexts + else + [] + end) + |> Par_List.map (fn ((action, context), command) => apply_action action context command) + |> ignore; + + (* finalize actions *) + List.app (uncurry finalize_action) contexts + end end); diff -r c10fe904ac10 -r 58f6b41efe88 src/HOL/Tools/Mirabelle/mirabelle.scala --- a/src/HOL/Tools/Mirabelle/mirabelle.scala Sun Jun 06 21:39:26 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Thu Jun 10 11:21:57 2021 +0200 @@ -33,49 +33,6 @@ } - /* exported log content */ - - object Log - { - def export_name(index: Int, theory: String = ""): String = - Export.compound_name(theory, "mirabelle/" + index) - - val separator = "\n------------------\n" - - sealed abstract class Entry { def print: String } - - case class Action(name: String, arguments: Properties.T, body: XML.Body) extends Entry - { - def print: String = "action: " + XML.content(body) + separator - } - case class Command(name: String, position: Properties.T, body: XML.Body) extends Entry - { - def print: String = "\n" + print_head + separator + Pretty.string_of(body) - def print_head: String = - { - val line = Position.Line.get(position) - val offset = Position.Offset.get(position) - val loc = line.toString + ":" + offset.toString - "at " + loc + " (" + name + "):" - } - } - case class Report(result: Properties.T, body: XML.Body) extends Entry - { - override def print: String = "\n" + separator + Pretty.string_of(body) - } - - def entry(export_name: String, xml: XML.Tree): Entry = - xml match { - case XML.Elem(Markup("action", (Markup.NAME, name) :: props), body) => - Action(name, props, body) - case XML.Elem(Markup("command", (Markup.NAME, name) :: props), body) => - Command(name, props.filter(Markup.position_property), body) - case XML.Elem(Markup("report", props), body) => Report(props, body) - case _ => error("Malformed export " + quote(export_name) + "\nbad XML: " + xml) - } - } - - /* main mirabelle */ def mirabelle( @@ -92,6 +49,7 @@ verbose: Boolean = false): Build.Results = { require(!selection.requirements) + Isabelle_System.make_directory(output_dir) progress.echo("Building required heaps ...") val build_results0 = @@ -107,41 +65,48 @@ ("mirabelle_theories=" + theories.mkString(",")) progress.echo("Running Mirabelle ...") - val build_results = - Build.build(build_options, clean_build = true, - selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs, - numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose) - if (build_results.ok) { - val structure = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs) - val store = Sessions.store(build_options) + val structure = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs) + val store = Sessions.store(build_options) - using(store.open_database_context())(db_context => - { - var seen_theories = Set.empty[String] - for { - session <- structure.imports_selection(selection).iterator - session_hierarchy = structure.hierarchy(session) - theories <- db_context.input_database(session)((db, a) => Some(store.read_theories(db, a))) - theory <- theories - if !seen_theories(theory) - index <- 1 to actions.length - export <- db_context.read_export(session_hierarchy, theory, Log.export_name(index)) - body = export.uncompressed_yxml - if body.nonEmpty - } { - seen_theories += theory - val export_name = Log.export_name(index, theory = theory) - val log = body.map(Log.entry(export_name, _)) - val log_dir = Isabelle_System.make_directory(output_dir + Path.basic(theory)) - val log_file = log_dir + Path.basic("mirabelle" + index).log - progress.echo("Writing " + log_file) - File.write(log_file, terminate_lines(log.map(_.print))) + def session_setup(session_name: String, session: Session): Unit = + { + val session_hierarchy = structure.hierarchy(session_name) + session.all_messages += + Session.Consumer[Prover.Message]("mirabelle_export") { + case msg: Prover.Protocol_Output => + msg.properties match { + case Protocol.Export(args) if args.name.startsWith("mirabelle/") => + if (verbose) { + progress.echo( + "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")") + } + using(store.open_database_context())(db_context => + { + for (export <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) { + val prefix = args.name.split('/') match { + case Array("mirabelle", action, "finalize") => + s"${action} finalize " + case Array("mirabelle", action, "goal", goal_name, line, offset) => + s"${action} goal.${goal_name} ${args.theory_name} ${line}:${offset} " + case _ => "" + } + val lines = Pretty.string_of(export.uncompressed_yxml).trim() + val body = Library.prefix_lines(prefix, lines) + "\n" + val log_file = output_dir + Path.basic("mirabelle.log") + File.append(log_file, body) + } + }) + case _ => + } + case _ => } - }) } - build_results + Build.build(build_options, clean_build = true, + selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs, + numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose, + session_setup = session_setup) } else build_results0 } @@ -171,6 +136,7 @@ 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") @@ -183,12 +149,13 @@ -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 + """) - -T THEORY theory restriction: NAME or NAME[LINE:END_LINE] + -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 + """) -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 + """) @@ -219,6 +186,7 @@ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), + "m:" -> (arg => options = options + ("mirabelle_max_calls=" + arg)), "o:" -> (arg => options = options + arg), "s:" -> (arg => options = options + ("mirabelle_stride=" + arg)), "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)), diff -r c10fe904ac10 -r 58f6b41efe88 src/HOL/Tools/Mirabelle/mirabelle_arith.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Sun Jun 06 21:39:26 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Thu Jun 10 11:21:57 2021 +0200 @@ -1,17 +1,24 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Jasmin Blanchette, TU Munich + Author: Sascha Boehme, TU Munich Author: Makarius + Author: Martin Desharnais, UniBw Munich Mirabelle action: "arith". *) -structure Mirabelle_Arith: sig end = +structure Mirabelle_Arith: MIRABELLE_ACTION = struct -val _ = - Theory.setup (Mirabelle.command_action \<^binding>\arith\ - (fn {timeout, ...} => fn {pre, ...} => - if Mirabelle.can_apply timeout Arith_Data.arith_tac pre - then "succeeded" else "")); +fun make_action ({timeout, ...} : Mirabelle.action_context) = + let + fun run_action ({pre, ...} : Mirabelle.command) = + if Mirabelle.can_apply timeout Arith_Data.arith_tac pre then + "succeeded" + else + "" + in {run_action = run_action, finalize = K ""} end + +val () = Mirabelle.register_action "arith" make_action end diff -r c10fe904ac10 -r 58f6b41efe88 src/HOL/Tools/Mirabelle/mirabelle_metis.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Sun Jun 06 21:39:26 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Thu Jun 10 11:21:57 2021 +0200 @@ -1,15 +1,17 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_metis.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Jasmin Blanchette, TU Munich + Author: Sascha Boehme, TU Munich + Author: Martin Desharnais, UniBw Munich Mirabelle action: "metis". *) -structure Mirabelle_Metis: sig end = +structure Mirabelle_Metis: MIRABELLE_ACTION = struct -val _ = - Theory.setup (Mirabelle.command_action \<^binding>\metis\ - (fn {timeout, ...} => fn {pre, post, ...} => +fun make_action ({timeout, ...} : Mirabelle.action_context) = + let + fun run_action ({pre, post, ...} : Mirabelle.command) = let val thms = Mirabelle.theorems_of_sucessful_proof post; val names = map Thm.get_name_hint thms; @@ -18,6 +20,9 @@ in (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |> not (null names) ? suffix (":\n" ^ commas names) - end)); + end + in {run_action = run_action, finalize = K ""} end + +val () = Mirabelle.register_action "metis" make_action end diff -r c10fe904ac10 -r 58f6b41efe88 src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML Sun Jun 06 21:39:26 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML Thu Jun 10 11:21:57 2021 +0200 @@ -1,23 +1,26 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Jasmin Blanchette, TU Munich + Author: Sascha Boehme, TU Munich + Author: Martin Desharnais, UniBw Munich Mirabelle action: "quickcheck". *) -structure Mirabelle_Quickcheck: sig end = +structure Mirabelle_Quickcheck: MIRABELLE_ACTION = struct -val _ = - Theory.setup (Mirabelle.command_action \<^binding>\quickcheck\ - (fn {arguments, timeout, ...} => fn {pre, ...} => - let - val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst; - val quickcheck = - Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key arguments)) 1; - in - (case Timeout.apply timeout quickcheck pre of - NONE => "no counterexample" - | SOME _ => "counterexample found") - end)); +fun make_action ({arguments, timeout, ...} : Mirabelle.action_context) = + let + val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst + val quickcheck = + Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key arguments)) 1 + + fun run_action ({pre, ...} : Mirabelle.command) = + (case Timeout.apply timeout quickcheck pre of + NONE => "no counterexample" + | SOME _ => "counterexample found") + in {run_action = run_action, finalize = K ""} end + +val () = Mirabelle.register_action "quickcheck" make_action end diff -r c10fe904ac10 -r 58f6b41efe88 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Sun Jun 06 21:39:26 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Thu Jun 10 11:21:57 2021 +0200 @@ -1,11 +1,14 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML - Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich + Author: Jasmin Blanchette, TU Munich + Author: Sascha Boehme, TU Munich + Author: Tobias Nipkow, TU Munich Author: Makarius + Author: Martin Desharnais, UniBw Munich Mirabelle action: "sledgehammer". *) -structure Mirabelle_Sledgehammer: sig end = +structure Mirabelle_Sledgehammer: MIRABELLE_ACTION = struct (*To facilitate synching the description of Mirabelle Sledgehammer parameters @@ -23,7 +26,6 @@ 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 lam_transK = "lam_trans" (*=STRING: lambda translation scheme*) -val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*) val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*) val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*) val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*) @@ -40,8 +42,6 @@ val type_encK = "type_enc" (*=STRING: type encoding scheme*) val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*) -val separator = "-----" - (*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*) (*defaults used in this Mirabelle action*) val preplay_timeout_default = "1" @@ -52,7 +52,6 @@ val strict_default = "false" val max_facts_default = "smart" val slice_default = "true" -val max_calls_default = 10000000 val check_trivial_default = false (*If a key is present in args then augment a list with its pair*) @@ -193,7 +192,7 @@ fun inc_proof_method_time t = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) + => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) val inc_proof_method_timeout = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) @@ -218,90 +217,62 @@ fun avg_time t n = if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 -fun log_sh_data (ShData - {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail}) = - let - val props = - [("sh_calls", str calls), - ("sh_success", str success), - ("sh_nontriv_calls", str nontriv_calls), - ("sh_nontriv_success", str nontriv_success), - ("sh_lemmas", str lemmas), - ("sh_max_lems", str max_lems), - ("sh_time_isa", str3 (ms time_isa)), - ("sh_time_prover", str3 (ms time_prover)), - ("sh_time_prover_fail", str3 (ms time_prover_fail))] - val text = - "\nTotal number of sledgehammer calls: " ^ str calls ^ - "\nNumber of successful sledgehammer calls: " ^ str success ^ - "\nNumber of sledgehammer lemmas: " ^ str lemmas ^ - "\nMax number of sledgehammer lemmas: " ^ str max_lems ^ - "\nSuccess rate: " ^ percentage success calls ^ "%" ^ - "\nTotal number of nontrivial sledgehammer calls: " ^ str nontriv_calls ^ - "\nNumber of successful nontrivial sledgehammer calls: " ^ str nontriv_success ^ - "\nTotal time for sledgehammer calls (Isabelle): " ^ str3 (ms time_isa) ^ - "\nTotal time for successful sledgehammer calls (ATP): " ^ str3 (ms time_prover) ^ - "\nTotal time for failed sledgehammer calls (ATP): " ^ str3 (ms time_prover_fail) ^ - "\nAverage time for sledgehammer calls (Isabelle): " ^ - str3 (avg_time time_isa calls) ^ - "\nAverage time for successful sledgehammer calls (ATP): " ^ - str3 (avg_time time_prover success) ^ - "\nAverage time for failed sledgehammer calls (ATP): " ^ - str3 (avg_time time_prover_fail (calls - success)) - in (props, text) end +fun log_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, + time_prover, time_prover_fail}) = + "\nTotal number of sledgehammer calls: " ^ str calls ^ + "\nNumber of successful sledgehammer calls: " ^ str success ^ + "\nNumber of sledgehammer lemmas: " ^ str lemmas ^ + "\nMax number of sledgehammer lemmas: " ^ str max_lems ^ + "\nSuccess rate: " ^ percentage success calls ^ "%" ^ + "\nTotal number of nontrivial sledgehammer calls: " ^ str nontriv_calls ^ + "\nNumber of successful nontrivial sledgehammer calls: " ^ str nontriv_success ^ + "\nTotal time for sledgehammer calls (Isabelle): " ^ str3 (ms time_isa) ^ + "\nTotal time for successful sledgehammer calls (ATP): " ^ str3 (ms time_prover) ^ + "\nTotal time for failed sledgehammer calls (ATP): " ^ str3 (ms time_prover_fail) ^ + "\nAverage time for sledgehammer calls (Isabelle): " ^ + str3 (avg_time time_isa calls) ^ + "\nAverage time for successful sledgehammer calls (ATP): " ^ + str3 (avg_time time_prover success) ^ + "\nAverage time for failed sledgehammer calls (ATP): " ^ + str3 (avg_time time_prover_fail (calls - success)) -fun log_re_data sh_calls (ReData {calls, success, nontriv_calls, - nontriv_success, proofs, time, timeout, lemmas = (lemmas, lems_sos, lems_max), posns}) = +fun log_re_data sh_calls (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, + timeout, lemmas = (lemmas, lems_sos, lems_max), posns}) = let val proved = posns |> map (fn (pos, triv) => str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ (if triv then "[T]" else "")) - val props = - [("re_calls", str calls), - ("re_success", str success), - ("re_nontriv_calls", str nontriv_calls), - ("re_nontriv_success", str nontriv_success), - ("re_proofs", str proofs), - ("re_time", str3 (ms time)), - ("re_timeout", str timeout), - ("re_lemmas", str lemmas), - ("re_lems_sos", str lems_sos), - ("re_lems_max", str lems_max), - ("re_proved", space_implode "," proved)] - val text = - "\nTotal number of proof method calls: " ^ str calls ^ - "\nNumber of successful proof method calls: " ^ str success ^ - " (proof: " ^ str proofs ^ ")" ^ - "\nNumber of proof method timeouts: " ^ str timeout ^ - "\nSuccess rate: " ^ percentage success sh_calls ^ "%" ^ - "\nTotal number of nontrivial proof method calls: " ^ str nontriv_calls ^ - "\nNumber of successful nontrivial proof method calls: " ^ str nontriv_success ^ - " (proof: " ^ str proofs ^ ")" ^ - "\nNumber of successful proof method lemmas: " ^ str lemmas ^ - "\nSOS of successful proof method lemmas: " ^ str lems_sos ^ - "\nMax number of successful proof method lemmas: " ^ str lems_max ^ - "\nTotal time for successful proof method calls: " ^ str3 (ms time) ^ - "\nAverage time for successful proof method calls: " ^ str3 (avg_time time success) ^ - "\nProved: " ^ space_implode " " proved - in (props, text) end + in + "\nTotal number of proof method calls: " ^ str calls ^ + "\nNumber of successful proof method calls: " ^ str success ^ + " (proof: " ^ str proofs ^ ")" ^ + "\nNumber of proof method timeouts: " ^ str timeout ^ + "\nSuccess rate: " ^ percentage success sh_calls ^ "%" ^ + "\nTotal number of nontrivial proof method calls: " ^ str nontriv_calls ^ + "\nNumber of successful nontrivial proof method calls: " ^ str nontriv_success ^ + " (proof: " ^ str proofs ^ ")" ^ + "\nNumber of successful proof method lemmas: " ^ str lemmas ^ + "\nSOS of successful proof method lemmas: " ^ str lems_sos ^ + "\nMax number of successful proof method lemmas: " ^ str lems_max ^ + "\nTotal time for successful proof method calls: " ^ str3 (ms time) ^ + "\nAverage time for successful proof method calls: " ^ str3 (avg_time time success) ^ + "\nProved: " ^ space_implode " " proved + end in -fun log_data index (Data {sh, re_u}) = +fun log_data (Data {sh, re_u}) = let val ShData {calls=sh_calls, ...} = sh val ReData {calls=re_calls, ...} = re_u in if sh_calls > 0 then - let - val (props1, text1) = log_sh_data sh - val (props2, text2) = log_re_data sh_calls re_u - val text = - "\n\nReport #" ^ string_of_int index ^ ":\n" ^ - (if re_calls > 0 then text1 ^ "\n" ^ text2 else text1) - in [Mirabelle.log_report (props1 @ props2) [XML.Text text]] end - else [] + let val text1 = log_sh_data sh in + if re_calls > 0 then text1 ^ "\n" ^ log_re_data sh_calls re_u else text1 + end + else + "" end end @@ -375,7 +346,7 @@ fun set_file_name (SOME dir) = Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix - ("prob_" ^ str0 (Position.line_of pos) ^ "__") + ("prob_" ^ StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "__") #> Config.put SMT_Config.debug_files (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_" ^ serial_string ()) @@ -457,9 +428,10 @@ in -fun run_sledgehammer change_data trivial args proof_method named_thms pos st = +fun run_sledgehammer change_data thy_index trivial args proof_method named_thms pos st = let val thy = Proof.theory_of st + val thy_name = Context.theory_name thy val triv_str = if trivial then "[T] " else "" val _ = change_data inc_sh_calls val _ = if trivial then () else change_data inc_sh_nontriv_calls @@ -482,6 +454,12 @@ 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 => + let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in + Path.append (Path.explode dir) (Path.basic subdir) + |> Isabelle_System.make_directory + |> Path.implode + end) 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 *) @@ -587,14 +565,14 @@ Mirabelle.can_apply timeout (do_method named_thms) st fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" - | with_time (true, t) = (change_data inc_proof_method_success; - if trivial then () - else change_data inc_proof_method_nontriv_success; - change_data (inc_proof_method_lemmas (length named_thms)); - change_data (inc_proof_method_time t); - change_data (inc_proof_method_posns (pos, trivial)); - if name = "proof" then change_data inc_proof_method_proofs else (); - "succeeded (" ^ string_of_int t ^ ")") + | with_time (true, t) = + (change_data inc_proof_method_success; + if trivial then () else change_data inc_proof_method_nontriv_success; + change_data (inc_proof_method_lemmas (length named_thms)); + change_data (inc_proof_method_time t); + change_data (inc_proof_method_posns (pos, trivial)); + if name = "proof" then change_data inc_proof_method_proofs else (); + "succeeded (" ^ string_of_int t ^ ")") fun timed_method named_thms = with_time (Mirabelle.cpu_time apply_method named_thms) handle Timeout.TIMEOUT _ => (change_data inc_proof_method_timeout; "timeout") @@ -606,70 +584,40 @@ val try_timeout = seconds 5.0 -fun catch e = - e () handle exn => - if Exn.is_interrupt exn then Exn.reraise exn - else Mirabelle.print_exn exn - -(* crude hack *) -val num_sledgehammer_calls = Unsynchronized.ref 0 +fun make_action ({arguments, timeout, ...} : Mirabelle.action_context) = + let + val check_trivial = + Mirabelle.get_bool_argument arguments (check_trivialK, check_trivial_default) -val _ = - Theory.setup (Mirabelle.theory_action \<^binding>\sledgehammer\ - (fn context => fn commands => - let - val {index, tag = sh_tag, arguments = args, timeout, ...} = context - fun proof_method_tag meth = "#" ^ string_of_int index ^ " " ^ meth ^ " (sledgehammer): " - - val data = Unsynchronized.ref empty_data - val change_data = Unsynchronized.change data - - val max_calls = Mirabelle.get_int_argument args (max_callsK, max_calls_default) - val check_trivial = Mirabelle.get_bool_argument args (check_trivialK, check_trivial_default) + val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data + val change_data = Synchronized.change data - val results = - commands |> maps (fn command => - let - val {name, pos, pre = st, ...} = command - val goal = Thm.major_prem_of (#goal (Proof.goal st)) - val log = - if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then [] - else - let - val _ = Unsynchronized.inc num_sledgehammer_calls - in - if !num_sledgehammer_calls > max_calls then - ["Skipping because max number of calls reached"] - else - let - val meth = Unsynchronized.ref "" - val named_thms = - Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) - val trivial = - if check_trivial then - Try0.try0 (SOME try_timeout) ([], [], [], []) st - handle Timeout.TIMEOUT _ => false - else false - val log1 = - sh_tag ^ catch (fn () => - run_sledgehammer change_data trivial args meth named_thms pos st) - val log2 = - (case ! named_thms of - SOME thms => - [separator, - proof_method_tag (!meth) ^ - catch (fn () => - run_proof_method change_data trivial false name meth thms - timeout pos st)] - | NONE => []) - in log1 :: log2 end - end - in - if null log then [] - else [Mirabelle.log_command command [XML.Text (cat_lines log)]] - end) + fun run_action ({theory_index, name, pos, pre, ...} : Mirabelle.command) = + let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in + if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then + "" + else + let + val meth = Unsynchronized.ref "" + val named_thms = + Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) + val trivial = + 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 + val log2 = + (case !named_thms of + SOME thms => + !meth ^ " (sledgehammer): " ^ run_proof_method change_data trivial false name meth + thms timeout pos pre + | NONE => "") + in log1 ^ "\n" ^ log2 end + end - val report = log_data index (! data) - in results @ report end)) + fun finalize () = log_data (Synchronized.value data) + in {run_action = run_action, finalize = finalize} end + +val () = Mirabelle.register_action "sledgehammer" make_action end diff -r c10fe904ac10 -r 58f6b41efe88 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML Sun Jun 06 21:39:26 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML Thu Jun 10 11:21:57 2021 +0200 @@ -1,11 +1,12 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Author: Jasmin Blanchette, TU Munich Author: Makarius + Author: Martin Desharnais, UniBw Munich Mirabelle action: "sledgehammer_filter". *) -structure Mirabelle_Sledgehammer_Filter: sig end = +structure Mirabelle_Sledgehammer_Filter: MIRABELLE_ACTION = struct fun get args name default_value = @@ -40,7 +41,7 @@ structure Prooftab = Table(type key = int * int val ord = prod_ord int_ord int_ord) -fun print_int x = Value.print_int (! x) +fun print_int x = Value.print_int (Synchronized.value x) fun percentage a b = if b = 0 then "N/A" else Value.print_int (a * 100 div b) fun percentage_alt a b = percentage a (a + b) @@ -51,133 +52,135 @@ val proof_fileK = "proof_file" -val _ = - Theory.setup (Mirabelle.theory_action \<^binding>\sledgehammer_filter\ - (fn context => fn commands => +fun make_action ({arguments, ...} : Mirabelle.action_context) = + let + val (proof_table, args) = let - val (proof_table, args) = - let - val (pf_args, other_args) = - #arguments context |> List.partition (curry (op =) proof_fileK o fst) - val proof_file = - (case pf_args of - [] => error "No \"proof_file\" specified" - | (_, s) :: _ => s) - fun do_line line = - (case line |> space_explode ":" of - [line_num, offset, proof] => - SOME (apply2 (the o Int.fromString) (line_num, offset), - proof |> space_explode " " |> filter_out (curry (op =) "")) - | _ => NONE) - val proof_table = - File.read (Path.explode proof_file) - |> space_explode "\n" - |> map_filter do_line - |> AList.coalesce (op =) - |> Prooftab.make - in (proof_table, other_args) end + val (pf_args, other_args) = + List.partition (curry (op =) proof_fileK o fst) arguments + val proof_file = + (case pf_args of + [] => error "No \"proof_file\" specified" + | (_, s) :: _ => s) + fun do_line line = + (case space_explode ":" line of + [line_num, offset, proof] => + SOME (apply2 (the o Int.fromString) (line_num, offset), + proof |> space_explode " " |> filter_out (curry (op =) "")) + | _ => NONE) + val proof_table = + File.read (Path.explode proof_file) + |> space_explode "\n" + |> map_filter do_line + |> AList.coalesce (op =) + |> Prooftab.make + in (proof_table, other_args) end - val num_successes = Unsynchronized.ref 0 - val num_failures = Unsynchronized.ref 0 - val num_found_proofs = Unsynchronized.ref 0 - val num_lost_proofs = Unsynchronized.ref 0 - val num_found_facts = Unsynchronized.ref 0 - val num_lost_facts = Unsynchronized.ref 0 + val num_successes = Synchronized.var "num_successes" 0 + val num_failures = Synchronized.var "num_failures" 0 + val num_found_proofs = Synchronized.var "num_found_proofs" 0 + val num_lost_proofs = Synchronized.var "num_lost_proofs" 0 + val num_found_facts = Synchronized.var "num_found_facts" 0 + val num_lost_facts = Synchronized.var "num_lost_facts" 0 + fun run_action ({pos, pre, ...} : Mirabelle.command) = + let val results = - commands |> maps (fn {pos, pre, ...} => - (case (Position.line_of pos, Position.offset_of pos) of - (SOME line_num, SOME offset) => - (case Prooftab.lookup proof_table (line_num, offset) of - SOME proofs => - let - val thy = Proof.theory_of pre - val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre - val prover = AList.lookup (op =) args "prover" |> the_default default_prover - val params as {max_facts, ...} = Sledgehammer_Commands.default_params thy args - val default_max_facts = - Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover - val relevance_fudge = - extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge - val subgoal = 1 - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt - val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover - val keywords = Thy_Header.get_keywords' ctxt - val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = - Sledgehammer_Fact.nearly_all_facts ctxt ho_atp - Sledgehammer_Fact.no_fact_override keywords css_table chained_ths - hyp_ts concl_t - |> Sledgehammer_Fact.drop_duplicate_facts - |> Sledgehammer_MePo.mepo_suggested_facts ctxt params - (the_default default_max_facts max_facts) - (SOME relevance_fudge) hyp_ts concl_t - |> map (fst o fst) - val (found_facts, lost_facts) = - flat proofs |> sort_distinct string_ord - |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) - |> List.partition (curry (op <=) 0 o fst) - |>> sort (prod_ord int_ord string_ord) ||> map snd - val found_proofs = filter (forall (member (op =) facts)) proofs - val n = length found_proofs - val log1 = - if n = 0 then - (Unsynchronized.inc num_failures; "Failure") - else - (Unsynchronized.inc num_successes; - Unsynchronized.add num_found_proofs n; - "Success (" ^ Value.print_int n ^ " of " ^ - Value.print_int (length proofs) ^ " proofs)") - val _ = Unsynchronized.add num_lost_proofs (length proofs - n) - val _ = Unsynchronized.add num_found_facts (length found_facts) - val _ = Unsynchronized.add num_lost_facts (length lost_facts) - val log2 = - if null found_facts then [] - else - let - val found_weight = - Real.fromInt (fold (fn (n, _) => Integer.add (n * n)) found_facts 0) - / Real.fromInt (length found_facts) - |> Math.sqrt |> Real.ceil - in - ["Found facts (among " ^ Value.print_int (length facts) ^ - ", weight " ^ Value.print_int found_weight ^ "): " ^ - commas (map with_index found_facts)] - end - val log3 = - if null lost_facts then [] - else - ["Lost facts (among " ^ Value.print_int (length facts) ^ "): " ^ - commas lost_facts] - in [XML.Text (cat_lines (log1 :: log2 @ log3))] end - | NONE => [XML.Text "No known proof"]) - | _ => [])) + (case (Position.line_of pos, Position.offset_of pos) of + (SOME line_num, SOME offset) => + (case Prooftab.lookup proof_table (line_num, offset) of + SOME proofs => + let + val thy = Proof.theory_of pre + val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre + val prover = AList.lookup (op =) args "prover" |> the_default default_prover + val params as {max_facts, ...} = Sledgehammer_Commands.default_params thy args + val default_max_facts = + Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover + val relevance_fudge = + extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge + val subgoal = 1 + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt + val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover + val keywords = Thy_Header.get_keywords' ctxt + val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt + val facts = + Sledgehammer_Fact.nearly_all_facts ctxt ho_atp + Sledgehammer_Fact.no_fact_override keywords css_table chained_ths + hyp_ts concl_t + |> Sledgehammer_Fact.drop_duplicate_facts + |> Sledgehammer_MePo.mepo_suggested_facts ctxt params + (the_default default_max_facts max_facts) + (SOME relevance_fudge) hyp_ts concl_t + |> map (fst o fst) + val (found_facts, lost_facts) = + flat proofs |> sort_distinct string_ord + |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) + |> List.partition (curry (op <=) 0 o fst) + |>> sort (prod_ord int_ord string_ord) ||> map snd + val found_proofs = filter (forall (member (op =) facts)) proofs + val n = length found_proofs + val _ = Int.div + val _ = Synchronized.change num_failures (curry op+ 1) + val log1 = + if n = 0 then + (Synchronized.change num_failures (curry op+ 1); "Failure") + else + (Synchronized.change num_successes (curry op+ 1); + Synchronized.change num_found_proofs (curry op+ n); + "Success (" ^ Value.print_int n ^ " of " ^ + Value.print_int (length proofs) ^ " proofs)") + val _ = Synchronized.change num_lost_proofs (curry op+ (length proofs - n)) + val _ = Synchronized.change num_found_facts (curry op+ (length found_facts)) + val _ = Synchronized.change num_lost_facts (curry op+ (length lost_facts)) + val log2 = + if null found_facts then + "" + else + let + val found_weight = + Real.fromInt (fold (fn (n, _) => Integer.add (n * n)) found_facts 0) + / Real.fromInt (length found_facts) + |> Math.sqrt |> Real.ceil + in + "Found facts (among " ^ Value.print_int (length facts) ^ + ", weight " ^ Value.print_int found_weight ^ "): " ^ + commas (map with_index found_facts) + end + val log3 = + if null lost_facts then + "" + else + "Lost facts (among " ^ Value.print_int (length facts) ^ "): " ^ + commas lost_facts + in cat_lines [log1, log2, log3] end + | NONE => "No known proof") + | _ => "") + in + results + end - val report = - if ! num_successes + ! num_failures > 0 then - let - val props = - [("num_successes", print_int num_successes), - ("num_failures", print_int num_failures), - ("num_found_proofs", print_int num_found_proofs), - ("num_lost_proofs", print_int num_lost_proofs), - ("num_found_facts", print_int num_found_facts), - ("num_lost_facts", print_int num_lost_facts)] - val text = - "\nNumber of overall successes: " ^ print_int num_successes ^ - "\nNumber of overall failures: " ^ print_int num_failures ^ - "\nOverall success rate: " ^ - percentage_alt (! num_successes) (! num_failures) ^ "%" ^ - "\nNumber of found proofs: " ^ print_int num_found_proofs ^ - "\nNumber of lost proofs: " ^ print_int num_lost_proofs ^ - "\nProof found rate: " ^ - percentage_alt (! num_found_proofs) (! num_lost_proofs) ^ "%" ^ - "\nNumber of found facts: " ^ print_int num_found_facts ^ - "\nNumber of lost facts: " ^ print_int num_lost_facts ^ - "\nFact found rate: " ^ - percentage_alt (! num_found_facts) (! num_lost_facts) ^ "%" - in [Mirabelle.log_report props [XML.Text text]] end - else [] - in results @ report end)) + fun finalize () = + if Synchronized.value num_successes + Synchronized.value num_failures > 0 then + "\nNumber of overall successes: " ^ print_int num_successes ^ + "\nNumber of overall failures: " ^ print_int num_failures ^ + "\nOverall success rate: " ^ + percentage_alt (Synchronized.value num_successes) + (Synchronized.value num_failures) ^ "%" ^ + "\nNumber of found proofs: " ^ print_int num_found_proofs ^ + "\nNumber of lost proofs: " ^ print_int num_lost_proofs ^ + "\nProof found rate: " ^ + percentage_alt (Synchronized.value num_found_proofs) + (Synchronized.value num_lost_proofs) ^ "%" ^ + "\nNumber of found facts: " ^ print_int num_found_facts ^ + "\nNumber of lost facts: " ^ print_int num_lost_facts ^ + "\nFact found rate: " ^ + percentage_alt (Synchronized.value num_found_facts) + (Synchronized.value num_lost_facts) ^ "%" + else + "" + in {run_action = run_action, finalize = finalize} end + +val () = Mirabelle.register_action "sledgehammer_filter" make_action end diff -r c10fe904ac10 -r 58f6b41efe88 src/HOL/Tools/Mirabelle/mirabelle_try0.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Sun Jun 06 21:39:26 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Thu Jun 10 11:21:57 2021 +0200 @@ -1,17 +1,25 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_try0.ML Author: Jasmin Blanchette, TU Munich Author: Makarius + Author: Martin Desharnais, UniBw Munich Mirabelle action: "try0". *) -structure Mirabelle_Try0 : sig end = +structure Mirabelle_Try0: MIRABELLE_ACTION = struct -val _ = - Theory.setup (Mirabelle.command_action \<^binding>\try0\ - (fn {timeout, ...} => fn {pre, ...} => - if Timeout.apply (Time.scale 10.0 timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre - then "succeeded" else "")); +fun make_action ({timeout, ...} : Mirabelle.action_context) = + let + val generous_timeout = Time.scale 10.0 timeout + + fun run_action ({pre, ...} : Mirabelle.command) = + if Timeout.apply generous_timeout (Try0.try0 (SOME timeout) ([], [], [], [])) pre then + "succeeded" + else + "" + in {run_action = run_action, finalize = K ""} end + +val () = Mirabelle.register_action "try0" make_action end diff -r c10fe904ac10 -r 58f6b41efe88 src/HOL/Tools/etc/options --- a/src/HOL/Tools/etc/options Sun Jun 06 21:39:26 2021 +0200 +++ b/src/HOL/Tools/etc/options Thu Jun 10 11:21:57 2021 +0200 @@ -56,6 +56,9 @@ option mirabelle_stride : int = 1 -- "default stride for running Mirabelle actions on every nth goal" +option mirabelle_max_calls : int = 10000000 + -- "default max. no. of calls to each Mirabelle action" + option mirabelle_actions : string = "" -- "Mirabelle actions (outer syntax, separated by semicolons)"