--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 24 09:12:09 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 24 11:02:42 2013 +0200
@@ -273,7 +273,7 @@
"subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
else
"goal")) [Logic.list_implies (nondef_assm_ts, orig_t)]))
- val _ = spying spy (fn () => "starting " ^ @{make_string} mode ^ " mode")
+ val _ = spying spy (fn () => (state, i, "starting " ^ @{make_string} mode ^ " mode"))
val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S"
o Date.fromTimeLocal o Time.now)
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
@@ -1055,7 +1055,7 @@
val _ = print_v (fn () =>
"Total time: " ^ string_of_time (Timer.checkRealTimer timer) ^
".")
- val _ = spying spy (fn () => "outcome: " ^ outcome_code)
+ val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code))
in (outcome_code, !state_ref) end
(* Give the inner timeout a chance. *)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 24 09:12:09 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 24 11:02:42 2013 +0200
@@ -629,7 +629,6 @@
fun register_codatatype_generic co_T case_name constr_xs generic =
let
- val ctxt = Context.proof_of generic
val thy = Context.theory_of generic
val {frac_types, ersatz_table, codatatypes} = Data.get generic
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Sep 24 09:12:09 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Sep 24 11:02:42 2013 +0200
@@ -53,7 +53,6 @@
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
val string_of_time : Time.time -> string
- val spying : bool -> (unit -> string) -> unit
val nat_subscript : int -> string
val flip_polarity : polarity -> polarity
val prop_T : typ
@@ -79,6 +78,7 @@
val unyxml : string -> string
val pretty_maybe_quote : Pretty.T -> Pretty.T
val hash_term : term -> int
+ val spying : bool -> (unit -> Proof.state * int * string) -> unit
end;
structure Nitpick_Util : NITPICK_UTIL =
@@ -242,15 +242,6 @@
val parse_time_option = Sledgehammer_Util.parse_time_option
val string_of_time = ATP_Util.string_of_time
-val spying_version = "a"
-
-fun spying false _ = ()
- | spying true f =
- let val message = f () in
- File.append (Path.explode "$ISABELLE_HOME_USER/spy_nitpick")
- (spying_version ^ " " ^ timestamp () ^ ": " ^ message ^ "\n")
- end
-
val subscript = implode o map (prefix "\<^sub>") o Symbol.explode
fun nat_subscript n =
n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
@@ -325,4 +316,20 @@
val hash_term = Word.toInt o hashw_term
+val hackish_string_of_term = Sledgehammer_Util.hackish_string_of_term
+
+val spying_version = "b"
+
+fun spying false _ = ()
+ | spying true f =
+ let
+ val (state, i, message) = f ()
+ val ctxt = Proof.context_of state
+ val goal = Logic.get_goal (prop_of (#goal (Proof.goal state))) i
+ val hash = String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12)
+ in
+ File.append (Path.explode "$ISABELLE_HOME_USER/spy_nitpick")
+ (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ message ^ "\n")
+ end
+
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Sep 24 09:12:09 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Sep 24 11:02:42 2013 +0200
@@ -271,9 +271,6 @@
is_package_def name orelse exists (fn s => String.isSuffix s name) blist
in is_blisted end
-fun hackish_string_of_term ctxt =
- with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
-
(* This is a terrible hack. Free variables are sometimes coded as "M__" when
they are displayed as "M" and we want to avoid clashes with these. But
sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Sep 24 09:12:09 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Sep 24 11:02:42 2013 +0200
@@ -73,7 +73,7 @@
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 _ = spying spy (fn () => (state, subgoal, 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)
@@ -116,7 +116,7 @@
print_used_facts used_facts used_from
| _ => ())
|> spy
- ? tap (fn res => spying spy (fn () => (name, spying_str_of_res res)))
+ ? tap (fn res => spying spy (fn () => (state, subgoal, 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
@@ -225,7 +225,8 @@
SOME name => error ("No such prover: " ^ name ^ ".")
| NONE => ()
val _ = print "Sledgehammering..."
- val _ = spying spy (fn () => ("***", "starting " ^ @{make_string} mode ^ " mode"))
+ val _ =
+ spying spy (fn () => (state, i, "***", "starting " ^ @{make_string} mode ^ " mode"))
val (smts, (ueq_atps, full_atps)) =
provers |> List.partition (is_smt_prover ctxt)
||> List.partition (is_unit_equational_atp ctxt)
@@ -242,8 +243,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"));
+ val _ = spying spy (fn () => (state, i, label ^ "s",
+ "filtering " ^ string_of_int (length all_facts) ^ " facts"));
in
all_facts
|> (case is_appropriate_prop of
@@ -259,7 +260,8 @@
else
())
|> spy ? tap (fn factss =>
- spying spy (fn () => (label ^ "s", "selected facts: " ^ spying_str_of_factss factss)))
+ spying spy (fn () =>
+ (state, i, label ^ "s", "selected facts: " ^ spying_str_of_factss factss)))
end
fun launch_provers state label is_appropriate_prop provers =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Sep 24 09:12:09 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Sep 24 11:02:42 2013 +0200
@@ -17,7 +17,6 @@
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 :
@@ -27,6 +26,8 @@
val one_year : Time.time
val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
+ val hackish_string_of_term : Proof.context -> term -> string
+ val spying : bool -> (unit -> Proof.state * int * string * string) -> unit
(** extrema **)
val max : ('a * 'a -> order) -> 'a -> 'a -> 'a
@@ -88,15 +89,6 @@
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 () =
@@ -167,6 +159,23 @@
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
(print_mode_value ())) f x
+fun hackish_string_of_term ctxt =
+ with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
+
+val spying_version = "b"
+
+fun spying false _ = ()
+ | spying true f =
+ let
+ val (state, i, tool, message) = f ()
+ val ctxt = Proof.context_of state
+ val goal = Logic.get_goal (prop_of (#goal (Proof.goal state))) i
+ val hash = String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12)
+ in
+ File.append (Path.explode "$ISABELLE_HOME_USER/spy_sledgehammer")
+ (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ tool ^ ": " ^ message ^ "\n")
+ end
+
(** extrema **)
fun max ord x y = case ord(x,y) of LESS => y | _ => x