# HG changeset patch # User blanchet # Date 1643641763 -3600 # Node ID b55d84e41d612ee30aaea75cc9cbdfee9f9b10cb # Parent 8d08bc7e8f984c79ab1d75ded1009daf7aaa9736 tweaked verbose output diff -r 8d08bc7e8f98 -r b55d84e41d61 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100 @@ -36,6 +36,9 @@ ML_file \Tools/Sledgehammer/sledgehammer_tactics.ML\ (* +lemma "1 + 1 = 3" + sledgehammer[verbose] + lemma "1 + 1 = 2" sledgehammer [slices = 40, max_proofs = 40] diff -r 8d08bc7e8f98 -r b55d84e41d61 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100 @@ -135,12 +135,20 @@ (used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play))) fun launch_prover (params as {verbose, spy, ...}) mode learn - (problem as {state, subgoal, factss, ...} : prover_problem) slice name = + (problem as {state, subgoal, factss, ...} : prover_problem) + (slice as ((num_facts, fact_filter), _)) name = let val ctxt = Proof.context_of state val _ = spying spy (fn () => (state, subgoal, name, "Launched")) + val _ = + if verbose then + writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^ + plural_s num_facts ^ "...") + else + () + fun print_used_facts used_facts used_from = tag_list 1 used_from |> map (fn (j, fact) => fact |> apsnd (K j)) @@ -164,7 +172,7 @@ fun filter_info (fact_filter, facts) = let val indices = find_indices facts - (* "Int.max" is there for robustness -- it shouldn't be necessary *) + (* "Int.max" is there for robustness *) val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?" in (commas (indices @ unknowns), fact_filter) @@ -182,11 +190,11 @@ | spying_str_of_res {outcome = SOME failure, ...} = "Failure: " ^ string_of_atp_failure failure in - get_minimizing_prover ctxt mode learn name params problem slice - |> 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))) + get_minimizing_prover ctxt mode learn name params problem slice + |> 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 @@ -245,8 +253,7 @@ val message = message () val () = (case outcome of - SH_Some _ => - the_default writeln writeln_result (prover_name ^ ": " ^ message) + SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message) | _ => ()) in (outcome, message) diff -r 8d08bc7e8f98 -r b55d84e41d61 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Jan 31 16:09:23 2022 +0100 @@ -73,7 +73,6 @@ | NONE => (false, false)) fun repair_context ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver name) - |> Config.put SMT_Config.verbose debug |> Config.put SMT_Config.higher_order higher_order |> Config.put SMT_Config.nat_as_int nat_as_int |> (if overlord then