--- 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 \<open>Tools/Mirabelle/mirabelle.ML\<close>
+
+ML \<open>
+signature MIRABELLE_ACTION = sig
+ val make_action : Mirabelle.action_context -> Mirabelle.action
+end
+\<close>
+
ML_file \<open>Tools/Mirabelle/mirabelle_arith.ML\<close>
ML_file \<open>Tools/Mirabelle/mirabelle_metis.ML\<close>
ML_file \<open>Tools/Mirabelle/mirabelle_quickcheck.ML\<close>
@@ -15,4 +24,4 @@
ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\<close>
ML_file \<open>Tools/Mirabelle/mirabelle_try0.ML\<close>
-end
+end
\ No newline at end of file
--- 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>\<open>mirabelle_timeout\<close>;
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_actions = Options.default_string \<^system_option>\<open>mirabelle_actions\<close>;
val mirabelle_theories = Options.default_string \<^system_option>\<open>mirabelle_theories\<close>;
@@ -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);
--- 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)),
--- 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>\<open>arith\<close>
- (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
--- 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>\<open>metis\<close>
- (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
--- 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>\<open>quickcheck\<close>
- (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
--- 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>\<open>sledgehammer\<close>
- (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
--- 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>\<open>sledgehammer_filter\<close>
- (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
--- 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>\<open>try0\<close>
- (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
--- 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)"