# HG changeset patch # User desharna # Date 1639908921 -3600 # Node ID 6f5eafd952c964abd34d8019757992d57549c425 # Parent 74c53a9027e291d11387a6ce4802eb24b35a9ea3# Parent 7ada0c20379bd08ed86c33dc4301924eef7f4a31 merged diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Mirabelle.thy --- a/src/HOL/Mirabelle.thy Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Mirabelle.thy Sun Dec 19 11:15:21 2021 +0100 @@ -13,7 +13,7 @@ ML \ signature MIRABELLE_ACTION = sig - val make_action : Mirabelle.action_context -> Mirabelle.action + val make_action : Mirabelle.action_context -> string * Mirabelle.action end \ diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Dec 19 11:15:21 2021 +0100 @@ -429,8 +429,7 @@ Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x val add_schematic_consts_of = Term.fold_aterms (fn Const (x as (s, _)) => - not (member (op =) atp_widely_irrelevant_consts s) - ? add_schematic_const x + not (is_widely_irrelevant_const s) ? add_schematic_const x | _ => I) fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Mirabelle/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/mirabelle.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Dec 19 11:15:21 2021 +0100 @@ -14,7 +14,7 @@ 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 + val register_action: string -> (action_context -> string * action) -> unit (*utility functions*) val print_exn: exn -> string @@ -71,7 +71,7 @@ local val actions = Synchronized.var "Mirabelle.actions" - (Symtab.empty : (action_context -> action) Symtab.table); + (Symtab.empty : (action_context -> string * action) Symtab.table); in fun register_action name make_action = @@ -100,6 +100,21 @@ fun make_action_path ({index, label, name, ...} : action_context) = Path.basic (if label = "" then string_of_int index ^ "." ^ name else label); +fun initialize_action (make_action : action_context -> string * action) context = + let + val (s, action) = make_action context + val action_path = make_action_path context; + val export_name = + Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "initialize"); + val () = + if s <> "" then + Export.export \<^theory> export_name [XML.Text s] + else + () + in + action + end + fun finalize_action ({finalize, ...} : action) context = let val s = run_action_function finalize; @@ -232,7 +247,7 @@ {index = n, label = label, name = name, arguments = args, timeout = mirabelle_timeout, output_dir = output_dir}; in - (make_action context, context) + (initialize_action make_action context, context) end); in (* run actions on all relevant goals *) diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Mirabelle/mirabelle.scala --- a/src/HOL/Tools/Mirabelle/mirabelle.scala Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Sun Dec 19 11:15:21 2021 +0100 @@ -85,7 +85,8 @@ val lines = Pretty.string_of(yxml).trim() val prefix = Export.explode_name(args.name) match { - case List("mirabelle", action, "finalize") => action + " finalize " + case List("mirabelle", action, "initialize") => action + " initialize " + case List("mirabelle", action, "finalize") => action + " finalize " case List("mirabelle", action, "goal", goal_name, line, offset) => action + " goal." + String.format("%-5s", goal_name) + " " + args.theory_name + " " + line + ":" + offset + " " diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Mirabelle/mirabelle_arith.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Sun Dec 19 11:15:21 2021 +0100 @@ -16,7 +16,7 @@ (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_action = run_action, finalize = K ""}) end val () = Mirabelle.register_action "arith" make_action diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Mirabelle/mirabelle_metis.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Sun Dec 19 11:15:21 2021 +0100 @@ -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_action = run_action, finalize = K ""}) end val () = Mirabelle.register_action "metis" make_action diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Mirabelle/mirabelle_presburger.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML Sun Dec 19 11:15:21 2021 +0100 @@ -14,7 +14,7 @@ (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_action = run_action, finalize = K ""}) end val () = Mirabelle.register_action "presburger" make_action diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML Sun Dec 19 11:15:21 2021 +0100 @@ -19,7 +19,7 @@ (case Timeout.apply timeout quickcheck pre of NONE => "no counterexample" | SOME _ => "counterexample found") - in {run_action = run_action, finalize = K ""} end + in ("", {run_action = run_action, finalize = K ""}) end val () = Mirabelle.register_action "quickcheck" make_action diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Sun Dec 19 11:15:21 2021 +0100 @@ -24,7 +24,6 @@ val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) val keepK = "keep" (*=BOOL: keep temporary files created by sledgehammer*) val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (e.g. using metis)*) -val proverK = "prover" (*=STRING: name of the external prover to call*) val term_orderK = "term_order" (*=STRING: term order (in E)*) (*defaults used in this Mirabelle action*) @@ -39,8 +38,7 @@ lemmas: int, max_lems: int, time_isa: int, - time_prover: int, - time_prover_fail: int} + time_prover: int} datatype re_data = ReData of { calls: int, @@ -56,11 +54,10 @@ fun make_sh_data (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, - time_prover,time_prover_fail) = + time_prover) = ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, - time_isa=time_isa, time_prover=time_prover, - time_prover_fail=time_prover_fail} + time_isa=time_isa, time_prover=time_prover} fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, timeout,lemmas,posns) = @@ -68,13 +65,12 @@ nontriv_success=nontriv_success, proofs=proofs, time=time, timeout=timeout, lemmas=lemmas, posns=posns} -val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0) +val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0) val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) -fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, - lemmas, max_lems, time_isa, - time_prover, time_prover_fail}) = (calls, success, nontriv_calls, - nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) +fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, + time_isa, time_prover}) = + (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, @@ -104,40 +100,37 @@ fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); val inc_sh_calls = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) - => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => + (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover)) val inc_sh_success = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) - => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => + (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover)) val inc_sh_nontriv_calls = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) - => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => + (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover)) val inc_sh_nontriv_success = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) - => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => + (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover)) fun inc_sh_lemmas n = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => + (calls, success, nontriv_calls, nontriv_success, lemmas+n, max_lems, time_isa, time_prover)) fun inc_sh_max_lems n = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => + (calls, success,nontriv_calls, nontriv_success, lemmas, Int.max (max_lems, n), time_isa, + time_prover)) fun inc_sh_time_isa t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => + (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa + t, time_prover)) fun inc_sh_time_prover t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) - -fun inc_sh_time_prover_fail t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => + (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover + t)) val inc_proof_method_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) @@ -187,7 +180,7 @@ 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}) = + time_prover}) = "\nTotal number of sledgehammer calls: " ^ str calls ^ "\nNumber of successful sledgehammer calls: " ^ str success ^ "\nNumber of sledgehammer lemmas: " ^ str lemmas ^ @@ -197,13 +190,10 @@ "\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)) + str3 (avg_time time_prover success) fun log_re_data sh_calls (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas = (lemmas, lems_sos, lems_max), posns}) = @@ -246,24 +236,6 @@ end -fun get_prover_name thy args = - let - fun default_prover_name () = - hd (#provers (Sledgehammer_Commands.default_params thy [])) - handle List.Empty => error "No ATP available" - in - (case AList.lookup (op =) args proverK of - SOME name => name - | NONE => default_prover_name ()) - end - -fun get_prover ctxt name params goal = - let - val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal) - in - Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name - end - type stature = ATP_Problem_Generate.stature fun is_good_line s = @@ -299,17 +271,8 @@ local -datatype sh_result = - SH_OK of int * int * (string * stature) list | - SH_FAIL of int * int | - SH_ERROR - -fun run_sh (params as {max_facts, minimize, preplay_timeout, ...}) prover_name e_selection_heuristic - term_order force_sos hard_timeout dir pos st = +fun run_sh params e_selection_heuristic term_order force_sos dir pos state = let - val thy = Proof.theory_of st - val {context = ctxt, facts = chained_ths, goal} = Proof.goal st - val i = 1 fun set_file_name (SOME dir) = let val filename = "prob_" ^ @@ -321,8 +284,8 @@ #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ()) end | set_file_name NONE = I - val st' = - st + val state' = + state |> Proof.map_context (set_file_name dir #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic) @@ -331,57 +294,20 @@ term_order |> the_default I) #> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos) force_sos |> the_default I)) - val default_max_facts = - Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt - val time_limit = - (case hard_timeout of - NONE => I - | SOME t => Timeout.apply t) - fun failed failure = - ({outcome = SOME failure, used_facts = [], used_from = [], - preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime, - message = K ""}, ~1) - val ({outcome, used_facts, preferred_methss, run_time, message, ...} - : Sledgehammer_Prover.prover_result, - time_isa) = time_limit (Mirabelle.cpu_time (fn () => - let - val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name - 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 - val factss = - facts - |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name - (the_default default_max_facts max_facts) - Sledgehammer_Fact.no_fact_override hyp_ts concl_t - |> tap (fn factss => - "Line " ^ str0 (Position.line_of pos) ^ ": " ^ - Sledgehammer.string_of_factss factss - |> writeln) - val prover = get_prover ctxt prover_name params goal - val problem = - {comment = "", state = st', goal = goal, subgoal = i, - subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss, found_proof = I} - in prover params problem end)) () - handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut - | Fail "inappropriate" => failed ATP_Proof.Inappropriate - val time_prover = run_time |> Time.toMilliseconds - val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts - st' i preferred_methss) + + val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () => + Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1 + Sledgehammer_Fact.no_fact_override state') () in - (case outcome of - NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) - | SOME _ => (msg, SH_FAIL (time_isa, time_prover))) + (sledgehammer_outcome, msg, cpu_time) end - handle ERROR msg => ("error: " ^ msg, SH_ERROR) + handle + ERROR msg => (Sledgehammer.SH_Unknown, " error: " ^ msg, 0) + | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0) in -fun run_sledgehammer change_data (params as {provers, timeout, ...}) output_dir +fun run_sledgehammer change_data (params as {provers, ...}) output_dir e_selection_heuristic term_order force_sos keep proof_method_from_msg thy_index trivial proof_method named_thms pos st = let @@ -400,17 +326,15 @@ end else NONE - (* always use a hard timeout, but give some slack so that the automatic - minimizer has a chance to do its magic *) - val hard_timeout = SOME (Time.scale 4.0 timeout) val prover_name = hd provers - val (msg, result) = - run_sh params prover_name e_selection_heuristic term_order force_sos hard_timeout keep_dir pos - st - in - (case result of - SH_OK (time_isa, time_prover, names) => + val (sledgehamer_outcome, msg, cpu_time) = + run_sh params e_selection_heuristic term_order force_sos keep_dir pos st + val outcome_msg = + (case sledgehamer_outcome of + Sledgehammer.SH_Some {used_facts, run_time, ...} => let + val num_used_facts = length used_facts + val time_prover = Time.toMilliseconds run_time fun get_thms (name, stature) = try (Sledgehammer_Util.thms_of_name (Proof.context_of st)) name @@ -418,21 +342,19 @@ in change_data inc_sh_success; if trivial then () else change_data inc_sh_nontriv_success; - change_data (inc_sh_lemmas (length names)); - change_data (inc_sh_max_lems (length names)); - change_data (inc_sh_time_isa time_isa); + 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 names); - triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ - string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg + named_thms := SOME (map_filter get_thms used_facts); + " (" ^ string_of_int cpu_time ^ "+" ^ string_of_int time_prover ^ ")" ^ + " [" ^ prover_name ^ "]:\n" end - | SH_FAIL (time_isa, time_prover) => - let - val _ = change_data (inc_sh_time_isa time_isa) - val _ = change_data (inc_sh_time_prover_fail time_prover) - in triv_str ^ "failed: " ^ msg end - | SH_ERROR => "failed: " ^ msg) + | _ => "") + in + change_data (inc_sh_time_isa cpu_time); + Sledgehammer.short_string_of_sledgehammer_outcome sledgehamer_outcome ^ " " ^ + triv_str ^ outcome_msg ^ msg end end @@ -531,11 +453,13 @@ |> (fn (params as {provers, ...}) => (case provers of prover :: _ => Sledgehammer_Prover.set_params_provers params [prover] - | _ => error "sledgehammer action requires one prover")) + | _ => 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) = 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 @@ -561,8 +485,8 @@ end fun finalize () = log_data (Synchronized.value data) - in {run_action = run_action, finalize = finalize} end + in (init_msg, {run_action = run_action, finalize = finalize}) end val () = Mirabelle.register_action "sledgehammer" make_action -end \ No newline at end of file +end diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML Sun Dec 19 11:15:21 2021 +0100 @@ -179,7 +179,7 @@ (Synchronized.value num_lost_facts) ^ "%" else "" - in {run_action = run_action, finalize = finalize} end + in ("", {run_action = run_action, finalize = finalize}) end val () = Mirabelle.register_action "sledgehammer_filter" make_action diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Mirabelle/mirabelle_try0.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Sun Dec 19 11:15:21 2021 +0100 @@ -18,7 +18,7 @@ "succeeded" else "" - in {run_action = run_action, finalize = K ""} end + in ("", {run_action = run_action, finalize = K ""}) end val () = Mirabelle.register_action "try0" make_action diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Dec 19 11:15:21 2021 +0100 @@ -15,17 +15,21 @@ type play_outcome = Sledgehammer_Proof_Methods.play_outcome type mode = Sledgehammer_Prover.mode type params = Sledgehammer_Prover.params + type induction_rules = Sledgehammer_Prover.induction_rules + type prover_problem = Sledgehammer_Prover.prover_problem + type prover_result = Sledgehammer_Prover.prover_result - val someN : string - val noneN : string - val timeoutN : string - val unknownN : string + datatype sledgehammer_outcome = SH_Some of prover_result | SH_Unknown | SH_Timeout | SH_None + val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string + + val induction_rules_for_prover : Proof.context -> string -> induction_rules option -> + induction_rules val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int -> proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome) val string_of_factss : (string * fact list) list -> string val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override -> - Proof.state -> bool * (string * string list) + Proof.state -> bool * (sledgehammer_outcome * string) end; structure Sledgehammer : SLEDGEHAMMER = @@ -45,20 +49,37 @@ open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh -val someN = "some" -val noneN = "none" -val timeoutN = "timeout" -val unknownN = "unknown" +datatype sledgehammer_outcome = SH_Some of prover_result | SH_Unknown | SH_Timeout | SH_None + +fun is_sledgehammer_outcome_some (SH_Some _) = true + | is_sledgehammer_outcome_some _ = false -val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN] +fun short_string_of_sledgehammer_outcome (SH_Some _) = "some" + | short_string_of_sledgehammer_outcome SH_Unknown = "unknown" + | short_string_of_sledgehammer_outcome SH_Timeout = "timeout" + | short_string_of_sledgehammer_outcome SH_None = "none" + +fun alternative f (SOME x) (SOME y) = SOME (f (x, y)) + | alternative _ (x as SOME _) NONE = x + | alternative _ NONE (y as SOME _) = y + | alternative _ NONE NONE = NONE -fun max_outcome_code codes = - NONE - |> fold (fn candidate => - fn accum as SOME _ => accum - | NONE => if member (op =) codes candidate then SOME candidate else NONE) - ordered_outcome_codes - |> the_default unknownN +fun max_outcome outcomes = + let + val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes + val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes + val timeout = find_first (fn (SH_Timeout, _) => true | _ => false) outcomes + val none = find_first (fn (SH_None, _) => true | _ => false) outcomes + in + some + |> alternative snd unknown + |> alternative snd timeout + |> alternative snd none + |> the_default (SH_Unknown, "") + end + +fun induction_rules_for_prover ctxt prover_name induction_rules = + the_default (if is_ho_atp ctxt prover_name then Include else Exclude) induction_rules fun is_metis_method (Metis_Method _) = true | is_metis_method _ = false @@ -115,26 +136,25 @@ |> (fn (used_facts, (meth, play)) => (used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play))) -fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout, - expect, induction_rules, ...}) mode writeln_result only learn - {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _, found_proof} name = +fun launch_prover (params as {verbose, spy, max_facts, induction_rules, ...}) mode only learn + ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem) name = let val ctxt = Proof.context_of state - val hard_timeout = Time.scale 5.0 timeout val _ = spying spy (fn () => (state, subgoal, name, "Launched")) val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name) - val num_facts = length facts |> not only ? Integer.min max_facts - val induction_rules = - the_default (if is_ho_atp ctxt name then Include else Exclude) induction_rules + val num_facts = + (case factss of + (_, facts) :: _ => length facts |> not only ? Integer.min max_facts + | _ => 0) + val induction_rules = induction_rules_for_prover ctxt name induction_rules val problem = {comment = comment, state = state, goal = goal, subgoal = subgoal, subgoal_count = subgoal_count, factss = factss - |> map (apsnd ((induction_rules = Exclude - ? filter_out (fn ((_, (_, Induction)), _) => true | _ => false)) - #> take num_facts)), + (* We take num_facts because factss contains the maximum of all called provers. *) + |> map (apsnd (take num_facts o maybe_filter_out_induction_rules induction_rules)), found_proof = found_proof} fun print_used_facts used_facts used_from = @@ -143,8 +163,8 @@ |> filter_used_facts false used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas - |> prefix ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ - " proof (of " ^ string_of_int (length facts) ^ "): ") + |> prefix ("Fact" ^ plural_s num_facts ^ " in " ^ quote name ^ + " proof (of " ^ string_of_int num_facts ^ "): ") |> writeln fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = @@ -178,58 +198,77 @@ end | spying_str_of_res {outcome = SOME failure, ...} = "Failure: " ^ string_of_atp_failure failure + in + problem + |> get_minimizing_prover ctxt mode learn name params + |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => + print_used_facts used_facts used_from + | _ => ()) + |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) + end + +fun preplay_prover_result ({ minimize, preplay_timeout, ...} : params) state subgoal + (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) = + let + val output = + if outcome = SOME ATP_Proof.TimedOut then + SH_Timeout + else if is_some outcome then + SH_None + else + SH_Some result + fun output_message () = message (fn () => + play_one_line_proof minimize preplay_timeout used_facts state subgoal preferred_methss) + in + (output, output_message) + end + +fun check_expected_outcome ctxt prover_name expect outcome = + let + val outcome_code = short_string_of_sledgehammer_outcome outcome + in + (* The "expect" argument is deliberately ignored if the prover is + missing so that the "Metis_Examples" can be processed on any + machine. *) + if expect = "" orelse outcome_code = expect orelse + not (is_prover_installed ctxt prover_name) then + () + else + error ("Unexpected outcome: " ^ quote outcome_code) + end + +fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result only + learn (problem as {state, subgoal, ...}) prover_name = + let + val ctxt = Proof.context_of state + val hard_timeout = Time.scale 5.0 timeout fun really_go () = - problem - |> get_minimizing_prover ctxt mode learn name params - |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => - print_used_facts used_facts used_from - | _ => ()) - |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) - |> (fn {outcome, used_facts, preferred_methss, message, ...} => - (if outcome = SOME ATP_Proof.TimedOut then timeoutN - else if is_some outcome then noneN - else someN, - fn () => message (fn () => play_one_line_proof minimize preplay_timeout used_facts state - subgoal preferred_methss))) + launch_prover params mode only learn problem prover_name + |> preplay_prover_result params state subgoal fun go () = - let - val (outcome_code, message) = - if debug then - really_go () - else - (really_go () - handle - ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") - | exn => - if Exn.is_interrupt exn then Exn.reraise exn - else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n")) + if debug then + really_go () + else + (really_go () + handle + ERROR msg => (SH_Unknown, fn () => "Error: " ^ msg ^ "\n") + | exn => + if Exn.is_interrupt exn then Exn.reraise exn + else (SH_Unknown, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n")) - val _ = - (* The "expect" argument is deliberately ignored if the prover is - missing so that the "Metis_Examples" can be processed on any - machine. *) - if expect = "" orelse outcome_code = expect orelse - not (is_prover_installed ctxt name) then - () - else - error ("Unexpected outcome: " ^ quote outcome_code) - in (outcome_code, message) end + val (outcome, message) = Timeout.apply hard_timeout go () + val () = check_expected_outcome ctxt prover_name expect outcome + + val message = message () + val () = + if mode <> Auto_Try andalso is_sledgehammer_outcome_some outcome orelse mode = Normal then + the_default writeln writeln_result (quote prover_name ^ ": " ^ message) + else + () in - if mode = Auto_Try then - let val (outcome_code, message) = Timeout.apply timeout go () in - (outcome_code, if outcome_code = someN then [message ()] else []) - end - else - let - val (outcome_code, message) = Timeout.apply hard_timeout go () - val outcome = - if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else "" - val _ = - if outcome <> "" andalso is_some writeln_result then the writeln_result outcome - else writeln outcome - in (outcome_code, []) end + (outcome, message) end val auto_try_max_facts_divisor = 2 (* FUDGE *) @@ -251,7 +290,7 @@ error "No prover is set" else (case subgoal_count state of - 0 => (error "No subgoal!"; (false, (noneN, []))) + 0 => (error "No subgoal!"; (false, (SH_None, ""))) | n => let val _ = Proof.assert_backward state @@ -268,13 +307,11 @@ I val ctxt = Proof.context_of state - val keywords = Thy_Header.get_keywords' ctxt - val {facts = chained, goal, ...} = Proof.goal state + 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 inst_inducts = induction_rules = SOME Instantiate - val css = clasimpset_rule_table_of ctxt val all_facts = - nearly_all_facts ctxt inst_inducts fact_override keywords css chained hyp_ts concl_t + 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) @@ -311,24 +348,23 @@ {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = factss, found_proof = found_proof} val learn = mash_learn_proof ctxt params (Thm.prop_of goal) - val launch = launch_prover params mode writeln_result only learn + val launch = launch_prover_and_preplay params mode writeln_result only learn in if mode = Auto_Try then - (unknownN, []) - |> fold (fn prover => fn accum as (outcome_code, _) => - if outcome_code = someN then accum else launch problem prover) + (SH_Unknown, "") + |> fold (fn prover => fn accum as (SH_Some _, _) => accum | _ => launch problem prover) provers else - (learn chained; + (learn chained_thms; provers - |> Par_List.map (launch problem #> fst) - |> max_outcome_code |> rpair []) + |> Par_List.map (launch problem) + |> max_outcome) end in launch_provers () handle Timeout.TIMEOUT _ => - (print "Sledgehammer ran out of time"; (unknownN, [])) + (print "Sledgehammer ran out of time"; (SH_Timeout, "")) end - |> `(fn (outcome_code, _) => outcome_code = someN)) + |> `(fn (outcome, _) => is_sledgehammer_outcome_some outcome)) end; diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sun Dec 19 11:15:21 2021 +0100 @@ -384,7 +384,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (((150, ""), THF (Polymorphic, {with_ite = true, with_let = true}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], + K [(1.0, (((512, ""), TH1, "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sun Dec 19 11:15:21 2021 +0100 @@ -394,6 +394,7 @@ val i = 1 in run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) + |> apsnd (map_prod short_string_of_sledgehammer_outcome single) end} val _ = diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Dec 19 11:15:21 2021 +0100 @@ -37,6 +37,8 @@ status Termtab.table -> lazy_fact list val nearly_all_facts : Proof.context -> bool -> fact_override -> Keyword.keywords -> status Termtab.table -> thm list -> term list -> term -> lazy_fact list + val nearly_all_facts_of_context : Proof.context -> bool -> fact_override -> thm list -> + term list -> term -> lazy_fact list val drop_duplicate_facts : lazy_fact list -> lazy_fact list end; @@ -554,6 +556,14 @@ |> inst_inducts ? instantiate_inducts ctxt hyp_ts concl_t end +fun nearly_all_facts_of_context ctxt inst_inducts fact_override = + let + val keywords = Thy_Header.get_keywords' ctxt + val css = clasimpset_rule_table_of ctxt + in + nearly_all_facts ctxt inst_inducts fact_override keywords css + end + fun drop_duplicate_facts facts = let val num_facts = length facts in facts |> num_facts <= max_facts_for_duplicates ? fact_distinct (op aconv) diff -r 7ada0c20379b -r 6f5eafd952c9 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Dec 17 16:36:42 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sun Dec 19 11:15:21 2021 +0100 @@ -19,6 +19,7 @@ datatype induction_rules = Include | Exclude | Instantiate val induction_rules_of_string : string -> induction_rules option + val maybe_filter_out_induction_rules : induction_rules -> fact list -> fact list type params = {debug : bool, @@ -47,6 +48,7 @@ preplay_timeout : Time.time, expect : string} + val string_of_params : params -> string val set_params_provers : params -> string list -> params type prover_problem = @@ -143,6 +145,13 @@ preplay_timeout : Time.time, expect : string} +fun string_of_params (params : params) = + YXML.content_of (ML_Pretty.string_of_polyml (ML_system_pretty (params, 100))) + +fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list = + induction_rules = Exclude ? + filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false) + fun set_params_provers params provers = {debug = #debug params, verbose = #verbose params,