# HG changeset patch # User blanchet # Date 1382035759 -7200 # Node ID f57f8e7a879f54a93bc9c280618ef6313ef0d9e0 # Parent 564b8adb095275fb94c8f2e59fd1d74186cafaef generate a comment storing the goal nickname in "learn_prover" diff -r 564b8adb0952 -r f57f8e7a879f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 17 20:20:53 2013 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 17 20:49:19 2013 +0200 @@ -493,7 +493,7 @@ |> Output.urgent_message) val prover = get_prover ctxt prover_name params goal facts val problem = - {state = st', goal = goal, subgoal = i, + {comment = "", state = st', goal = goal, subgoal = i, subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss} in prover params (K (K (K ""))) problem end)) () handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut diff -r 564b8adb0952 -r f57f8e7a879f src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Thu Oct 17 20:20:53 2013 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Thu Oct 17 20:49:19 2013 +0200 @@ -147,7 +147,7 @@ |> map fact_of_raw_fact val ctxt = ctxt |> set_file_name method prob_dir_name val res as {outcome, ...} = - run_prover_for_mash ctxt params prover facts goal + run_prover_for_mash ctxt params prover name facts goal val ok = if is_none outcome then 1 else 0 in (str_of_result method facts res, ok) end val ress = diff -r 564b8adb0952 -r f57f8e7a879f src/HOL/TPTP/sledgehammer_tactics.ML --- a/src/HOL/TPTP/sledgehammer_tactics.ML Thu Oct 17 20:20:53 2013 +0200 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Thu Oct 17 20:49:19 2013 +0200 @@ -42,7 +42,7 @@ concl_t |> hd |> snd val problem = - {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, + {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)]} in (case prover params (K (K (K ""))) problem of diff -r 564b8adb0952 -r f57f8e7a879f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Oct 17 20:20:53 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Oct 17 20:49:19 2013 +0200 @@ -60,7 +60,7 @@ val thm_less : thm * thm -> bool val goal_of_thm : theory -> thm -> thm val run_prover_for_mash : - Proof.context -> params -> string -> fact list -> thm -> prover_result + Proof.context -> params -> string -> string -> fact list -> thm -> prover_result val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> term list -> (string * real) list @@ -565,11 +565,11 @@ fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init -fun run_prover_for_mash ctxt params prover facts goal = +fun run_prover_for_mash ctxt params prover goal_name facts goal = let val problem = - {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, - factss = [("", facts)]} + {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1, + subgoal_count = 1, factss = [("", facts)]} in get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K ""))) problem @@ -762,6 +762,7 @@ let val thy = Proof_Context.theory_of ctxt val goal = goal_of_thm thy th + val name = nickname_of_thm th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt val facts = facts |> filter (fn (_, th') => thm_less (th', th)) fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th) @@ -783,13 +784,12 @@ val num_isar_deps = length isar_deps in if verbose andalso auto_level = 0 then - "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of_thm th) ^ - " with " ^ string_of_int num_isar_deps ^ " + " ^ - string_of_int (length facts - num_isar_deps) ^ " facts." + "MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^ string_of_int num_isar_deps ^ + " + " ^ string_of_int (length facts - num_isar_deps) ^ " facts." |> Output.urgent_message else (); - case run_prover_for_mash ctxt params prover facts goal of + case run_prover_for_mash ctxt params prover name facts goal of {outcome = NONE, used_facts, ...} => (if verbose andalso auto_level = 0 then let val num_facts = length used_facts in diff -r 564b8adb0952 -r f57f8e7a879f src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 17 20:20:53 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 17 20:49:19 2013 +0200 @@ -81,7 +81,8 @@ slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} val problem = - {state = state, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)]} + {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, + factss = [("", facts)]} val result as {outcome, used_facts, run_time, ...} = prover params (K (K (K ""))) problem in diff -r 564b8adb0952 -r f57f8e7a879f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Oct 17 20:20:53 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Oct 17 20:49:19 2013 +0200 @@ -45,7 +45,8 @@ expect : string} type prover_problem = - {state : Proof.state, + {comment : string, + state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, @@ -286,7 +287,8 @@ expect : string} type prover_problem = - {state : Proof.state, + {comment : string, + state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, @@ -563,7 +565,7 @@ max_new_mono_instances, isar_proofs, isar_compress, isar_try0, slice, timeout, preplay_timeout, ...}) minimize_command - ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = + ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state @@ -727,7 +729,8 @@ val _ = atp_problem |> lines_of_atp_problem format ord ord_info - |> cons ("% " ^ command ^ "\n") + |> cons ("% " ^ command ^ "\n" ^ + (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path val ((output, run_time), (atp_proof, outcome)) = time_limit generous_slice_timeout Isabelle_System.bash_output diff -r 564b8adb0952 -r f57f8e7a879f src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Oct 17 20:20:53 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Oct 17 20:49:19 2013 +0200 @@ -68,7 +68,7 @@ fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, slice, timeout, expect, ...}) mode output_result minimize_command only learn - {state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = + {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = let val ctxt = Proof.context_of state @@ -82,7 +82,7 @@ fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal val problem = - {state = state, goal = goal, subgoal = subgoal, + {comment = comment, state = state, goal = goal, subgoal = subgoal, subgoal_count = subgoal_count, factss = factss |> map (apsnd ((not (is_ho_atp ctxt name) @@ -282,7 +282,7 @@ let val factss = get_factss label is_appropriate_prop provers val problem = - {state = state, goal = goal, subgoal = i, subgoal_count = n, + {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = factss} fun learn prover = mash_learn_proof ctxt params prover (prop_of goal) all_facts