--- a/NEWS Mon Jan 24 21:29:37 2022 +0100
+++ b/NEWS Tue Jan 25 09:57:44 2022 +0100
@@ -54,6 +54,7 @@
- Added option "-r INT" to randomize the goals with a given seed before
selection.
- Added option "-y" for a dry run.
+ - Renamed run_action to run in Mirabelle.action record. Minor INCOMPATIBILITY.
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jan 25 09:57:44 2022 +0100
@@ -2083,14 +2083,14 @@
val hyp_ts = map freeze_term hyp_ts;
val concl_t = freeze_term concl_t;
+ val maybe_presimp_prop = presimp ? presimp_prop simp_options ctxt type_enc
- val facts = facts |> map (apsnd (pair Axiom))
+ val facts = facts |> map (apsnd (pair Axiom o maybe_presimp_prop))
val conjs =
map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)]
- |> map_index (apfst (rpair (Local, General) o string_of_int))
+ |> map_index (map_prod (rpair (Local, General) o string_of_int) (apsnd maybe_presimp_prop))
val ((conjs, facts), lam_facts) =
(conjs, facts)
- |> presimp ? apply2 (map (apsnd (apsnd (presimp_prop simp_options ctxt type_enc))))
|> (if lam_trans = no_lamsN then
rpair []
else
@@ -2834,7 +2834,8 @@
val app_op_level =
if completish > 0 then
Full_App_Op_And_Predicator
- else if length facts + length hyp_ts >= app_op_and_predicator_threshold then
+ else if is_greater_equal
+ (compare_length_with facts (app_op_and_predicator_threshold - length hyp_ts)) then
if is_type_enc_polymorphic type_enc then Min_App_Op else Sufficient_App_Op
else
Sufficient_App_Op_And_Predicator
--- a/src/HOL/Tools/ATP/atp_util.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Tue Jan 25 09:57:44 2022 +0100
@@ -49,6 +49,7 @@
val extract_lambda_def : (term -> string * typ) -> term -> string * term
val short_thm_name : Proof.context -> thm -> string
val map_prod : ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd
+ val compare_length_with : 'a list -> int -> order
end;
structure ATP_Util : ATP_UTIL =
@@ -412,6 +413,11 @@
else long
end
- val map_prod = Ctr_Sugar_Util.map_prod
+val map_prod = Ctr_Sugar_Util.map_prod
+
+(* Compare the length of a list with an integer n while traversing at most n elements of the list.
+*)
+fun compare_length_with [] n = if n < 0 then GREATER else if n = 0 then EQUAL else LESS
+ | compare_length_with (_ :: xs) n = if n <= 0 then GREATER else compare_length_with xs (n - 1)
end;
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Tue Jan 25 09:57:44 2022 +0100
@@ -13,7 +13,7 @@
output_dir: Path.T}
type command =
{theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}
- type action = {run_action: command -> string, finalize: unit -> string}
+ type action = {run: command -> string, finalize: unit -> string}
val register_action: string -> (action_context -> string * action) -> unit
(*utility functions*)
@@ -67,9 +67,9 @@
type action_context =
{index: int, label: string, name: string, arguments: Properties.T, timeout: Time.time,
output_dir: Path.T};
-type action = {run_action: command -> string, finalize: unit -> string};
+type action = {run: command -> string, finalize: unit -> string};
-val dry_run_action : action = {run_action = K "", finalize = K ""}
+val dry_run_action : action = {run = K "", finalize = K ""}
local
val actions = Synchronized.var "Mirabelle.actions"
@@ -130,14 +130,14 @@
()
end
-fun apply_action ({run_action, ...} : action) context (command as {pos, pre, ...} : command) =
+fun apply_action ({run, ...} : 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 ({elapsed, ...}, s) = Timing.timing run_action_function (fn () => run_action command);
+ val ({elapsed, ...}, s) = Timing.timing run_action_function (fn () => run command);
val export_name =
Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path +
line_path + offset_path + Path.basic (string_of_int (Time.toMilliseconds elapsed)));
--- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Tue Jan 25 09:57:44 2022 +0100
@@ -12,11 +12,11 @@
fun make_action ({timeout, ...} : Mirabelle.action_context) =
let
- fun run_action ({pre, ...} : Mirabelle.command) =
+ fun run ({pre, ...} : Mirabelle.command) =
(case Timing.timing (Mirabelle.can_apply timeout Arith_Data.arith_tac) pre of
({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
| (_, false) => "failed")
- in ("", {run_action = run_action, finalize = K ""}) end
+ in ("", {run = run, finalize = K ""}) end
val () = Mirabelle.register_action "arith" make_action
--- a/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Tue Jan 25 09:57:44 2022 +0100
@@ -11,7 +11,7 @@
fun make_action ({timeout, ...} : Mirabelle.action_context) =
let
- fun run_action ({pre, post, ...} : Mirabelle.command) =
+ fun run ({pre, post, ...} : Mirabelle.command) =
let
val thms = Mirabelle.theorems_of_sucessful_proof post;
val names = map Thm.get_name_hint thms;
@@ -21,7 +21,7 @@
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
|> not (null names) ? suffix (":\n" ^ commas names)
end
- in ("", {run_action = run_action, finalize = K ""}) end
+ in ("", {run = run, finalize = K ""}) end
val () = Mirabelle.register_action "metis" make_action
--- a/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML Tue Jan 25 09:57:44 2022 +0100
@@ -9,12 +9,11 @@
fun make_action ({timeout, ...} : Mirabelle.action_context) =
let
- val _ = Timing.timing
- fun run_action ({pre, ...} : Mirabelle.command) =
+ fun run ({pre, ...} : Mirabelle.command) =
(case Timing.timing (Mirabelle.can_apply timeout (Cooper.tac true [] [])) pre of
({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
| (_, false) => "failed")
- in ("", {run_action = run_action, finalize = K ""}) end
+ in ("", {run = run, finalize = K ""}) end
val () = Mirabelle.register_action "presburger" make_action
--- a/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML Tue Jan 25 09:57:44 2022 +0100
@@ -15,11 +15,11 @@
val quickcheck =
Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key arguments)) 1
- fun run_action ({pre, ...} : Mirabelle.command) =
+ fun run ({pre, ...} : Mirabelle.command) =
(case Timeout.apply timeout quickcheck pre of
NONE => "no counterexample"
| SOME _ => "counterexample found")
- in ("", {run_action = run_action, finalize = K ""}) end
+ in ("", {run = run, finalize = K ""}) end
val () = Mirabelle.register_action "quickcheck" make_action
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Tue Jan 25 09:57:44 2022 +0100
@@ -310,15 +310,12 @@
in
-fun run_sledgehammer change_data (params as {provers, ...}) output_dir
- e_selection_heuristic term_order force_sos keep_probs keep_proofs proof_method_from_msg thy_index
- trivial proof_method named_thms pos st =
+fun run_sledgehammer (params as {provers, ...}) output_dir e_selection_heuristic term_order
+ force_sos keep_probs keep_proofs proof_method_from_msg thy_index trivial 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
val keep =
if keep_probs orelse keep_proofs then
let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in
@@ -332,7 +329,7 @@
val prover_name = hd provers
val (sledgehamer_outcome, msg, cpu_time) =
run_sh params e_selection_heuristic term_order force_sos keep pos st
- val outcome_msg =
+ val (time_prover, change_data, proof_method_and_used_thms) =
(case sledgehamer_outcome of
Sledgehammer.SH_Some {used_facts, run_time, ...} =>
let
@@ -342,21 +339,24 @@
try (Sledgehammer_Util.thms_of_name (Proof.context_of st))
name
|> Option.map (pair (name, stature))
+ val change_data =
+ inc_sh_success
+ #> not trivial ? inc_sh_nontriv_success
+ #> inc_sh_lemmas num_used_facts
+ #> inc_sh_max_lems num_used_facts
+ #> inc_sh_time_prover time_prover
in
- change_data inc_sh_success;
- if trivial then () else change_data inc_sh_nontriv_success;
- change_data (inc_sh_lemmas num_used_facts);
- change_data (inc_sh_max_lems num_used_facts);
- change_data (inc_sh_time_prover time_prover);
- proof_method := proof_method_from_msg msg;
- named_thms := SOME (map_filter get_thms used_facts);
- " (" ^ string_of_int cpu_time ^ "+" ^ string_of_int time_prover ^ ")" ^
- " [" ^ prover_name ^ "]:\n"
+ (SOME time_prover, change_data,
+ SOME (proof_method_from_msg msg, map_filter get_thms used_facts))
end
- | _ => "")
+ | _ => (NONE, I, NONE))
+ val outcome_msg =
+ "(SH " ^ string_of_int cpu_time ^ "ms" ^
+ (case time_prover of NONE => "" | SOME ms => ", ATP " ^ string_of_int ms ^ "ms") ^
+ ") [" ^ prover_name ^ "]: "
in
- change_data (inc_sh_time_isa cpu_time);
- (sledgehamer_outcome, triv_str ^ outcome_msg ^ msg)
+ (sledgehamer_outcome, triv_str ^ outcome_msg ^ msg, change_data #> inc_sh_time_isa cpu_time,
+ proof_method_and_used_thms)
end
end
@@ -369,7 +369,7 @@
("slice", "false"),
("timeout", timeout |> Time.toSeconds |> string_of_int)]
-fun run_proof_method change_data trivial full name meth named_thms timeout pos st =
+fun run_proof_method trivial full name meth named_thms timeout pos st =
let
fun do_method named_thms ctxt =
let
@@ -385,58 +385,60 @@
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
(override_params prover type_enc (my_timeout time_slice)) fact_override []
in
- if !meth = "sledgehammer_tac" then
+ if meth = "sledgehammer_tac" then
sledge_tac 0.2 ATP_Proof.vampireN "mono_native"
ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??"
ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native"
ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??"
ORELSE' SMT_Solver.smt_tac ctxt thms
- else if !meth = "smt" then
+ else if meth = "smt" then
SMT_Solver.smt_tac ctxt thms
else if full then
Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN]
ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
- else if String.isPrefix "metis (" (!meth) then
+ else if String.isPrefix "metis (" meth then
let
val (type_encs, lam_trans) =
- !meth
+ meth
|> Token.explode (Thy_Header.get_keywords' ctxt) Position.start
|> filter Token.is_proper |> tl
|> Metis_Tactic.parse_metis_options |> fst
|>> the_default [ATP_Proof_Reconstruct.partial_typesN]
||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans
in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
- else if !meth = "metis" then
+ else if meth = "metis" then
Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
- else if !meth = "none" then
+ else if meth = "none" then
K all_tac
- else if !meth = "fail" then
+ else if meth = "fail" then
K no_tac
else
- (warning ("Unknown method " ^ quote (!meth)); K no_tac)
+ (warning ("Unknown method " ^ quote meth); K no_tac)
end
fun apply_method named_thms =
Mirabelle.can_apply timeout (do_method named_thms) st
- fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
+ fun with_time (false, t) = ("failed (" ^ string_of_int t ^ ")", I)
| 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 ^ ")")
+ ("succeeded (" ^ string_of_int t ^ ")",
+ inc_proof_method_success
+ #> not trivial ? inc_proof_method_nontriv_success
+ #> inc_proof_method_lemmas (length named_thms)
+ #> inc_proof_method_time t
+ #> inc_proof_method_posns (pos, trivial)
+ #> name = "proof" ? inc_proof_method_proofs)
fun timed_method named_thms =
with_time (Mirabelle.cpu_time apply_method named_thms)
- handle Timeout.TIMEOUT _ => (change_data inc_proof_method_timeout; "timeout")
- | ERROR msg => ("error: " ^ msg)
+ handle Timeout.TIMEOUT _ => ("timeout", inc_proof_method_timeout)
+ | ERROR msg => ("error: " ^ msg, I)
+ in
+ timed_method named_thms
+ |> apsnd (fn change_data => change_data
+ #> inc_proof_method_calls
+ #> not trivial ? inc_proof_method_nontriv_calls)
+ end
- val _ = change_data inc_proof_method_calls
- val _ = if trivial then () else change_data inc_proof_method_nontriv_calls
- in timed_method named_thms end
-
-val try_timeout = seconds 5.0
+val try0 = Try0.try0 (SOME (Time.fromSeconds 5)) ([], [], [], [])
fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) =
let
@@ -459,32 +461,27 @@
| _ => error "sledgehammer action requires one and only one prover"))
val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data
- val change_data = Synchronized.change data
val init_msg = "Params for sledgehammer: " ^ Sledgehammer_Prover.string_of_params params
- fun run_action ({theory_index, name, pos, pre, ...} : Mirabelle.command) =
+ fun run ({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 (outcome, log1) =
- run_sledgehammer change_data params output_dir e_selection_heuristic term_order
- force_sos keep_probs keep_proofs proof_method_from_msg theory_index trivial 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 => "")
+ val trivial = check_trivial andalso try0 pre handle Timeout.TIMEOUT _ => false
+ val (outcome, log1, change_data1, proof_method_and_used_thms) =
+ run_sledgehammer params output_dir e_selection_heuristic term_order
+ force_sos keep_probs keep_proofs proof_method_from_msg theory_index trivial pos pre
+ val (log2, change_data2) =
+ (case proof_method_and_used_thms of
+ SOME (proof_method, used_thms) =>
+ run_proof_method trivial false name proof_method used_thms timeout pos pre
+ |> apfst (prefix (proof_method ^ " (sledgehammer): "))
+ | NONE => ("", I))
+ val () = Synchronized.change data
+ (change_data1 #> change_data2 #> inc_sh_calls #> not trivial ? inc_sh_nontriv_calls)
in
log1 ^ "\n" ^ log2
|> Symbol.trim_blanks
@@ -493,7 +490,7 @@
end
fun finalize () = log_data (Synchronized.value data)
- in (init_msg, {run_action = run_action, finalize = finalize}) end
+ in (init_msg, {run = run, finalize = finalize}) end
val () = Mirabelle.register_action "sledgehammer" make_action
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML Tue Jan 25 09:57:44 2022 +0100
@@ -83,7 +83,7 @@
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) =
+ fun run ({pos, pre, ...} : Mirabelle.command) =
let
val results =
(case (Position.line_of pos, Position.offset_of pos) of
@@ -179,7 +179,7 @@
(Synchronized.value num_lost_facts) ^ "%"
else
""
- in ("", {run_action = run_action, finalize = finalize}) end
+ in ("", {run = run, finalize = finalize}) end
val () = Mirabelle.register_action "sledgehammer_filter" make_action
--- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Tue Jan 25 09:57:44 2022 +0100
@@ -13,12 +13,12 @@
let
val generous_timeout = Time.scale 10.0 timeout
- fun run_action ({pre, ...} : Mirabelle.command) =
+ fun run ({pre, ...} : Mirabelle.command) =
if Timeout.apply generous_timeout (Try0.try0 (SOME timeout) ([], [], [], [])) pre then
"succeeded"
else
""
- in ("", {run_action = run_action, finalize = K ""}) end
+ in ("", {run = run, finalize = K ""}) end
val () = Mirabelle.register_action "try0" make_action
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Jan 25 09:57:44 2022 +0100
@@ -310,14 +310,17 @@
val inst_inducts = induction_rules = SOME Instantiate
val {facts = chained_thms, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
- val all_facts =
- nearly_all_facts_of_context ctxt inst_inducts fact_override chained_thms hyp_ts concl_t
val _ =
(case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name)
| NONE => ())
val _ = print "Sledgehammering..."
val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode"))
+ val ({elapsed, ...}, all_facts) = Timing.timing
+ (nearly_all_facts_of_context ctxt inst_inducts fact_override chained_thms hyp_ts) concl_t
+ val _ = spying spy (fn () => (state, i, "All",
+ "Extracting " ^ string_of_int (length all_facts) ^ " facts from background theory in " ^
+ string_of_int (Time.toMilliseconds elapsed) ^ " ms"))
val spying_str_of_factss =
commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
@@ -330,15 +333,17 @@
| NONE =>
0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
|> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor))
- val _ = spying spy (fn () => (state, i, "All",
- "Filtering " ^ string_of_int (length all_facts) ^ " facts (MaSh algorithm: " ^
- str_of_mash_algorithm (the_mash_algorithm ()) ^ ")"));
+ val ({elapsed, ...}, factss) = Timing.timing
+ (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t)
+ all_facts
+ val () = spying spy (fn () => (state, i, "All",
+ "Filtering facts in " ^ string_of_int (Time.toMilliseconds elapsed) ^
+ " ms (MaSh algorithm: " ^ str_of_mash_algorithm (the_mash_algorithm ()) ^ ")"));
+ val () = if verbose then print (string_of_factss factss) else ()
+ val () = spying spy (fn () =>
+ (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))
in
- all_facts
- |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
- |> tap (fn factss => if verbose then print (string_of_factss factss) else ())
- |> spy ? tap (fn factss => spying spy (fn () =>
- (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
+ factss
end
fun launch_provers () =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Tue Jan 25 09:57:44 2022 +0100
@@ -657,7 +657,7 @@
known_failures = known_szs_status_failures,
prem_role = prem_role,
best_slices =
- K [(1.0, (((200, ""), format, type_enc,
+ K [(1.0, (((200, "mepo"), format, type_enc,
if is_format_higher_order format then keep_lamsN
else combsN, uncurried_aliases), ""))],
best_max_mono_iters = default_max_mono_iters,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Jan 25 09:57:44 2022 +0100
@@ -531,8 +531,7 @@
||> op @ |> op @
end
-fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts
- concl_t =
+fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts concl_t =
if only andalso null add then
[]
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 24 21:29:37 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Jan 25 09:57:44 2022 +0100
@@ -133,7 +133,7 @@
fun run_atp mode name
({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter,
max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs,
- slice, minimize, timeout, preplay_timeout, ...} : params)
+ slice, minimize, timeout, preplay_timeout, spy, ...} : params)
({comment, state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) =
let
val thy = Proof.theory_of state
@@ -254,7 +254,7 @@
|> writeln
else
()
- val value as (atp_problem, _, _, _) =
+ val ({elapsed, ...}, value as (atp_problem, _, _, _)) = Timing.timing (fn () =>
if cache_key = SOME key then
cache_value
else
@@ -272,7 +272,11 @@
|> map (apsnd Thm.prop_of)
|> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode
lam_trans uncurried_aliases readable_names true hyp_ts concl_t
- end
+ end) ()
+
+ val () = spying spy (fn () =>
+ (state, subgoal, name, "Slice #" ^ string_of_int (slice + 1) ^
+ " generating ATP problem in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms"))
fun sel_weights () = atp_problem_selection_weights atp_problem
fun ord_info () = atp_problem_term_order_info atp_problem
@@ -310,6 +314,10 @@
handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut))
| ERROR msg => (("", Time.zeroTime), ([], SOME (UnknownError msg)))
+ val () = spying spy (fn () =>
+ (state, subgoal, name, "Slice #" ^ string_of_int (slice + 1) ^
+ " running command in " ^ string_of_int (Time.toMilliseconds run_time) ^ " ms"))
+
val outcome =
(case outcome of
NONE =>