# HG changeset patch # User blanchet # Date 1459159547 -7200 # Node ID 23de054397e50876f0ebc6e35fe4cdcb1bf77ed1 # Parent 38fefd98c929c96d2a37c85d515ec7cec8142d3c early warning when Sledgehammer finds a proof diff -r 38fefd98c929 -r 23de054397e5 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Mar 28 12:05:47 2016 +0200 @@ -109,7 +109,7 @@ fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout, expect, ...}) mode writeln_result only learn - {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = + {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _, found_proof} name = let val ctxt = Proof.context_of state @@ -124,7 +124,8 @@ factss = factss |> map (apsnd ((not (is_ho_atp ctxt name) ? filter_out (fn ((_, (_, Induction)), _) => true | _ => false)) - #> take num_facts))} + #> take num_facts)), + found_proof = found_proof} fun print_used_facts used_facts used_from = tag_list 1 used_from @@ -244,8 +245,18 @@ | n => let val _ = Proof.assert_backward state - val print = - if mode = Normal andalso is_none writeln_result then writeln else K () + val print = if mode = Normal andalso is_none writeln_result then writeln else K () + + val found_proof = + if mode = Normal then + let val proof_found = Synchronized.var "proof_found" false in + fn () => + if Synchronized.change_result proof_found (rpair true) then () + else (writeln_result |> the_default writeln) "Proof found..." + end + else + I + val ctxt = Proof.context_of state val keywords = Thy_Header.get_keywords' ctxt val {facts = chained, goal, ...} = Proof.goal state @@ -288,7 +299,7 @@ val factss = get_factss provers val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, - factss = factss} + factss = factss, found_proof = found_proof} val learn = mash_learn_proof ctxt params (Thm.prop_of goal) all_facts val launch = launch_prover params mode writeln_result only learn in diff -r 38fefd98c929 -r 23de054397e5 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Mar 28 12:05:47 2016 +0200 @@ -834,7 +834,7 @@ let val problem = {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1, - subgoal_count = 1, factss = [("", facts)]} + subgoal_count = 1, factss = [("", facts)], found_proof = I} in get_minimizing_prover ctxt MaSh (K ()) prover params problem end diff -r 38fefd98c929 -r 23de054397e5 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Mar 28 12:05:47 2016 +0200 @@ -49,7 +49,8 @@ goal : thm, subgoal : int, subgoal_count : int, - factss : (string * fact list) list} + factss : (string * fact list) list, + found_proof : unit -> unit} type prover_result = {outcome : atp_failure option, @@ -133,7 +134,8 @@ goal : thm, subgoal : int, subgoal_count : int, - factss : (string * fact list) list} + factss : (string * fact list) list, + found_proof : unit -> unit} type prover_result = {outcome : atp_failure option, diff -r 38fefd98c929 -r 23de054397e5 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Mar 28 12:05:47 2016 +0200 @@ -133,7 +133,7 @@ ({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) - ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = + ({comment, state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state @@ -318,7 +318,7 @@ in if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure end - | NONE => NONE) + | NONE => (found_proof (); NONE)) | _ => outcome) in ((SOME key, value), (output, run_time, facts, atp_proof, outcome), diff -r 38fefd98c929 -r 23de054397e5 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Mar 28 12:05:47 2016 +0200 @@ -98,7 +98,7 @@ expect = ""} val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, - factss = [("", facts)]} + factss = [("", facts)], found_proof = I} val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, message} = prover params problem diff -r 38fefd98c929 -r 23de054397e5 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Mar 28 12:05:47 2016 +0200 @@ -180,7 +180,7 @@ fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs, minimize, preplay_timeout, ...}) - ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = + ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state @@ -199,6 +199,7 @@ (case outcome of NONE => let + val _ = found_proof (); val smt_method = smt_proofs <> SOME false val preferred_methss = (if smt_method then SMT_Method else Metis_Method (NONE, NONE),