# HG changeset patch # User blanchet # Date 1380013362 -7200 # Node ID e8aa538e959ed10473f961500228c6190f216f88 # Parent 255a2929c137561fac5d7343fc021f2d9abf55ef encode goal digest in spying log (to detect duplicates) diff -r 255a2929c137 -r e8aa538e959e src/HOL/Tools/Nitpick/nitpick.ML --- 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. *) diff -r 255a2929c137 -r e8aa538e959e src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r 255a2929c137 -r e8aa538e959e src/HOL/Tools/Nitpick/nitpick_util.ML --- 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; diff -r 255a2929c137 -r e8aa538e959e src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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 diff -r 255a2929c137 -r e8aa538e959e src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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 = diff -r 255a2929c137 -r e8aa538e959e src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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