--- 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
--- 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 =
--- 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
--- 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
--- 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
--- 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
--- 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