# HG changeset patch # User blanchet # Date 1306485007 -7200 # Node ID ff631c45797e73862b5f5d27a7b32eed37757f8a # Parent c96f06bffd90fd34b748ed7cf461aea1f954d196 make output more concise diff -r c96f06bffd90 -r ff631c45797e src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 27 10:30:07 2011 +0200 @@ -248,9 +248,7 @@ | minimize_line minimize_command ss = case minimize_command ss of "" => "" - | command => - "\nTo minimize the number of lemmas, try this: " ^ - Markup.markup Markup.sendback command ^ "." + | command => "\nTo minimize: " ^ Markup.markup Markup.sendback command ^ "." val split_used_facts = List.partition (curry (op =) Chained o snd) diff -r c96f06bffd90 -r ff631c45797e src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:07 2011 +0200 @@ -318,8 +318,10 @@ |> Exn.release |> tap (after path) -fun proof_banner auto = - if auto then "Auto Sledgehammer found a proof" else "Try this command" +fun proof_banner auto blocking name = + if auto then "Auto Sledgehammer (" ^ quote name ^ ") found a proof" + else if blocking then quote name ^ " found a proof" + else "Try this command" val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true) @@ -472,8 +474,8 @@ fun run_atp auto name ({exec, required_execs, arguments, proof_delims, known_failures, conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config) - ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters, - max_new_mono_instances, explicit_apply, isar_proof, + ({debug, verbose, overlord, blocking, type_sys, max_relevant, + max_mono_iters, max_new_mono_instances, explicit_apply, isar_proof, isar_shrink_factor, slicing, timeout, ...} : params) minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = let @@ -711,8 +713,8 @@ val isar_params = (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab) val metis_params = - (proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset, - fact_names, typed_helpers, goal, subgoal) + (proof_banner auto blocking name, minimize_command, type_sys, atp_proof, + facts_offset, fact_names, typed_helpers, goal, subgoal) val (outcome, (message, used_facts)) = case outcome of NONE => @@ -884,7 +886,8 @@ (Config.put Metis_Tactics.verbose debug #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i -fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command +fun run_smt_solver auto name (params as {debug, verbose, blocking, ...}) + minimize_command ({state, subgoal, subgoal_count, facts, smt_filter, ...} : prover_problem) = let @@ -907,7 +910,7 @@ ("smt", if name = SMT_Solver.solver_name_of ctxt then "" else "smt_solver = " ^ maybe_quote name) in - try_command_line (proof_banner auto) + try_command_line (proof_banner auto blocking name) (apply_on_subgoal settings subgoal subgoal_count ^ command_call method (map fst other_lemmas)) ^ minimize_line minimize_command diff -r c96f06bffd90 -r ff631c45797e src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:07 2011 +0200 @@ -104,7 +104,7 @@ max_relevant |> the_default (default_max_relevant_for_prover ctxt slicing name) val num_facts = length facts |> not only ? Integer.min max_relevant - val desc = + fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal val problem = {state = state, goal = goal, subgoal = subgoal, @@ -145,25 +145,28 @@ in (outcome_code, message) end in if auto then - let - val (outcome_code, message) = TimeLimit.timeLimit timeout go () - val success = (outcome_code = someN) - in - (success, state |> success ? Proof.goal_message (fn () => - Pretty.chunks [Pretty.str "", - Pretty.mark Markup.hilite (Pretty.str message)])) + let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in + (outcome_code, + state + |> outcome_code = someN + ? Proof.goal_message (fn () => + [Pretty.str "", + Pretty.mark Markup.hilite (Pretty.str message)] + |> Pretty.chunks)) end else if blocking then - let val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () in - Async_Manager.implode_desc desc ^ "\n" ^ message + let + val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () + in + (if outcome_code = someN then message else quote name ^ ": " ^ message) |> Async_Manager.break_into_chunks |> List.app Output.urgent_message; - (outcome_code = someN, state) + (outcome_code, state) end else - (Async_Manager.launch das_tool birth_time death_time desc + (Async_Manager.launch das_tool birth_time death_time (desc ()) (apfst (curry (op <>) timeoutN) o go); - (false, state)) + (unknownN, state)) end fun class_of_smt_solver ctxt name = @@ -216,7 +219,9 @@ facts = facts, smt_filter = maybe_smt_filter (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i} - val launch = launch_prover params auto minimize_command only + fun launch problem = + launch_prover params auto minimize_command only problem + #>> curry (op =) someN in if auto then fold (fn prover => fn (true, state) => (true, state)