--- a/src/HOL/Tools/ATP/atp_util.ML Mon Sep 23 13:34:15 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Mon Sep 23 14:53:43 2013 +0200
@@ -56,7 +56,11 @@
structure ATP_Util : ATP_UTIL =
struct
-val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
+fun timestamp_format time =
+ Date.fmt "%Y-%m-%d %H:%M:%S." (Date.fromTimeLocal time) ^
+ (StringCvt.padLeft #"0" 3 (string_of_int (Time.toMilliseconds time - 1000 * Time.toSeconds time)))
+
+val timestamp = timestamp_format o Time.now
(* This hash function is recommended in "Compilers: Principles, Techniques, and
Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Sep 23 13:34:15 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Sep 23 14:53:43 2013 +0200
@@ -81,6 +81,7 @@
[("debug", "false"),
("verbose", "false"),
("overlord", "false"),
+ ("spy", "false"),
("blocking", "false"),
("type_enc", "smart"),
("strict", "false"),
@@ -108,6 +109,7 @@
[("no_debug", "debug"),
("quiet", "verbose"),
("no_overlord", "overlord"),
+ ("dont_spy", "spy"),
("non_blocking", "blocking"),
("non_strict", "strict"),
("no_uncurried_aliases", "uncurried_aliases"),
@@ -184,7 +186,10 @@
structure Data = Theory_Data
(
type T = raw_param list
- val empty = default_default_params |> map (apsnd single)
+ val empty =
+ default_default_params
+ |> getenv "SLEDGEHAMMER_SPY" = "yes" ? AList.update (op =) ("spy", "true")
+ |> map (apsnd single)
val extend = I
fun merge data : T = AList.merge (op =) (K true) data
)
@@ -278,6 +283,7 @@
val debug = mode <> Auto_Try andalso lookup_bool "debug"
val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
+ val spy = lookup_bool "spy"
val blocking =
Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
lookup_bool "blocking"
@@ -311,15 +317,13 @@
else lookup_time "preplay_timeout"
val expect = lookup_string "expect"
in
- {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
- provers = provers, type_enc = type_enc, strict = strict,
- lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
- learn = learn, fact_filter = fact_filter, max_facts = max_facts,
- fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
+ {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,
+ provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
+ uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
+ max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice,
- minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
- expect = expect}
+ isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice, minimize = minimize,
+ timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
fun get_params mode = extract_params mode o default_raw_params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Sep 23 13:34:15 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Sep 23 14:53:43 2013 +0200
@@ -55,7 +55,7 @@
fun print silent f = if silent then () else Output.urgent_message (f ())
-fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
+fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters,
max_new_mono_instances, type_enc, strict, lam_trans,
uncurried_aliases, isar_proofs, isar_compress, isar_try0,
preplay_timeout, ...} : params)
@@ -73,18 +73,16 @@
val {goal, ...} = Proof.goal state
val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
val params =
- {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
- provers = provers, type_enc = type_enc, strict = strict,
- lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
- learn = false, fact_filter = NONE, max_facts = SOME (length facts),
- fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
- max_new_mono_instances = max_new_mono_instances,
- isar_proofs = isar_proofs, isar_compress = isar_compress,
- isar_try0 = isar_try0, slice = false, minimize = SOME false,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
+ {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true,
+ provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
+ uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
+ max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
+ max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
+ isar_proofs = isar_proofs, isar_compress = isar_compress, isar_try0 = isar_try0,
+ 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)]}
+ {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
@@ -248,7 +246,7 @@
end
fun adjust_reconstructor_params override_params
- ({debug, verbose, overlord, blocking, provers, type_enc, strict,
+ ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict,
lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
isar_compress, isar_try0, slice, minimize, timeout, preplay_timeout,
@@ -263,15 +261,13 @@
val type_enc = lookup_override "type_enc" type_enc
val lam_trans = lookup_override "lam_trans" lam_trans
in
- {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
- provers = provers, type_enc = type_enc, strict = strict,
- lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
- learn = learn, fact_filter = fact_filter, max_facts = max_facts,
- fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
+ {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,
+ provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
+ uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
+ max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice,
- minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
- expect = expect}
+ isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice, minimize = minimize,
+ timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
fun maybe_minimize ctxt mode do_learn name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Sep 23 13:34:15 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Sep 23 14:53:43 2013 +0200
@@ -22,6 +22,7 @@
{debug : bool,
verbose : bool,
overlord : bool,
+ spy : bool,
blocking : bool,
provers : string list,
type_enc : string option,
@@ -333,6 +334,7 @@
{debug : bool,
verbose : bool,
overlord : bool,
+ spy : bool,
blocking : bool,
provers : string list,
type_enc : string option,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Sep 23 13:34:15 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Sep 23 14:53:43 2013 +0200
@@ -30,6 +30,7 @@
open ATP_Util
open ATP_Problem_Generate
+open ATP_Proof
open ATP_Proof_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Fact
@@ -64,29 +65,31 @@
(if blocking then "."
else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
-fun launch_prover (params as {debug, verbose, blocking, max_facts, slice,
+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 =
let
val ctxt = Proof.context_of state
+
val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
+ val _ = spying spy (fn () => (name, "launched"));
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, hard_timeout)
- val max_facts =
- max_facts |> the_default (default_max_facts_of_prover ctxt slice name)
+ val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt slice name)
val num_facts = length facts |> not only ? Integer.min max_facts
- fun desc () =
- prover_description ctxt params name num_facts subgoal subgoal_count goal
+
+ fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal
+
val problem =
{state = state, goal = goal, subgoal = subgoal,
subgoal_count = subgoal_count,
- factss =
- factss
+ factss = factss
|> map (apsnd ((not (is_ho_atp ctxt name)
? filter_out (fn ((_, (_, Induction)), _) => true
| _ => false))
#> take num_facts))}
+
fun print_used_facts used_facts used_from =
tag_list 1 used_from
|> map (fn (j, fact) => fact |> apsnd (K j))
@@ -96,6 +99,15 @@
|> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
" proof (of " ^ string_of_int (length facts) ^ "): ") "."
|> Output.urgent_message
+
+ fun spying_str_of_res {outcome = NONE, used_facts, ...} =
+ let val num_used_facts = length used_facts in
+ "success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^
+ plural_s num_used_facts
+ end
+ | spying_str_of_res {outcome = SOME failure, ...} =
+ "failure: " ^ string_of_atp_failure failure
+
fun really_go () =
problem
|> get_minimizing_prover ctxt mode learn name params minimize_command
@@ -103,10 +115,13 @@
? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
print_used_facts used_facts used_from
| _ => ())
+ |> spy
+ ? tap (fn res => spying spy (fn () => (name, spying_str_of_res res)))
|> (fn {outcome, preplay, message, message_tail, ...} =>
(if outcome = SOME ATP_Proof.TimedOut then timeoutN
else if is_some outcome then noneN
else someN, fn () => message (Lazy.force preplay) ^ message_tail))
+
fun go () =
let
val (outcome_code, message) =
@@ -182,8 +197,7 @@
|> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
|> space_implode "\n\n"
-fun run_sledgehammer (params as {debug, verbose, blocking, provers, max_facts,
- slice, ...})
+fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, slice, ...})
mode output_result i (fact_override as {only, ...}) minimize_command state =
if null provers then
error "No prover is set."
@@ -211,9 +225,14 @@
SOME name => error ("No such prover: " ^ name ^ ".")
| NONE => ()
val _ = print "Sledgehammering..."
+ val _ = spying spy (fn () => ("***", "run"))
val (smts, (ueq_atps, full_atps)) =
provers |> List.partition (is_smt_prover ctxt)
||> List.partition (is_unit_equational_atp ctxt)
+
+ val spying_str_of_factss =
+ commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
+
fun get_factss label is_appropriate_prop provers =
let
val max_max_facts =
@@ -223,6 +242,8 @@
0 |> fold (Integer.max o default_max_facts_of_prover ctxt slice)
provers
|> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
+ val _ = spying spy (fn () =>
+ (label ^ "s", "filtering " ^ string_of_int (length all_facts) ^ " facts"));
in
all_facts
|> (case is_appropriate_prop of
@@ -237,7 +258,10 @@
|> print
else
())
+ |> spy ? tap (fn factss =>
+ spying spy (fn () => (label ^ "s", "selected facts: " ^ spying_str_of_factss factss)))
end
+
fun launch_provers state label is_appropriate_prop provers =
let
val factss = get_factss label is_appropriate_prop provers
@@ -260,6 +284,7 @@
|> (if blocking then Par_List.map else map) (launch problem #> fst)
|> max_outcome_code |> rpair state
end
+
fun launch_atps label is_appropriate_prop atps accum =
if null atps then
accum
@@ -274,15 +299,19 @@
accum)
else
launch_provers state label is_appropriate_prop atps
+
fun launch_smts accum =
if null smts then accum else launch_provers state "SMT solver" NONE smts
+
val launch_full_atps = launch_atps "ATP" NONE full_atps
- val launch_ueq_atps =
- launch_atps "Unit-equational provers" (SOME is_unit_equality) ueq_atps
+
+ val launch_ueq_atps = launch_atps "Unit-equational provers" (SOME is_unit_equality) ueq_atps
+
fun launch_atps_and_smt_solvers () =
[launch_full_atps, launch_smts, launch_ueq_atps]
|> Par_List.map (fn f => ignore (f (unknownN, state)))
handle ERROR msg => (print ("Error: " ^ msg); error msg)
+
fun maybe f (accum as (outcome_code, _)) =
accum |> (mode = Normal orelse outcome_code <> someN) ? f
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Sep 23 13:34:15 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Sep 23 14:53:43 2013 +0200
@@ -17,6 +17,7 @@
val time_mult : real -> Time.time -> Time.time
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
+ val spying : bool -> (unit -> string * string) -> unit
val subgoal_count : Proof.state -> int
val reserved_isar_keyword_table : unit -> unit Symtab.table
val thms_in_proof :
@@ -87,6 +88,15 @@
SOME (seconds (the secs))
end
+val spying_version = "a"
+
+fun spying false _ = ()
+ | spying true f =
+ let val (tool, message) = f () in
+ File.append (Path.explode "$ISABELLE_HOME_USER/spy_sledgehammer")
+ (spying_version ^ " " ^ timestamp () ^ ": " ^ tool ^ ": " ^ message ^ "\n")
+ end
+
val subgoal_count = Try.subgoal_count
fun reserved_isar_keyword_table () =