--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jun 26 16:41:43 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jun 26 18:57:20 2014 +0200
@@ -192,19 +192,12 @@
val auto_try_max_facts_divisor = 2 (* FUDGE *)
fun string_of_facts facts =
- "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
+ "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^
(facts |> map (fst o fst) |> space_implode " ") ^ "."
fun string_of_factss factss =
- if forall (null o snd) factss then
- "Found no relevant facts."
- else
- (case factss of
- [(_, facts)] => string_of_facts facts
- | _ =>
- factss
- |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
- |> space_implode "\n\n")
+ if forall (null o snd) factss then "Found no relevant facts."
+ else cat_lines (map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) factss)
fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode
output_result i (fact_override as {only, ...}) minimize_command state =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jun 26 16:41:43 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jun 26 18:57:20 2014 +0200
@@ -1714,10 +1714,13 @@
[("", [])]
else
let
- fun maybe_launch_thread () =
+ fun maybe_launch_thread min_num_facts_to_learn =
if not (Async_Manager.has_running_threads MaShN) andalso
Time.toSeconds timeout >= min_secs_for_learning then
let val timeout = time_mult learn_timeout_slack timeout in
+ Output.urgent_message ("Started MaShing through at least " ^
+ string_of_int min_num_facts_to_learn ^ " fact" ^ plural_s min_num_facts_to_learn ^
+ " in the background");
launch_thread timeout
(fn () => (true, mash_learn_facts ctxt params prover true 2 false timeout facts))
end
@@ -1729,8 +1732,9 @@
let
val {access_G, xtabs = ((num_facts0, _), _), ...} = peek_state ctxt overlord I
val is_in_access_G = is_fact_in_graph access_G o snd
+ val min_num_facts_to_learn = length facts - num_facts0
in
- if length facts - num_facts0 <= max_facts_to_learn_before_query then
+ if min_num_facts_to_learn <= max_facts_to_learn_before_query then
(case length (filter_out is_in_access_G facts) of
0 => false
| num_facts_to_learn =>
@@ -1739,9 +1743,9 @@
|> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s));
true)
else
- (maybe_launch_thread (); false))
+ (maybe_launch_thread num_facts_to_learn; false))
else
- (maybe_launch_thread (); false)
+ (maybe_launch_thread min_num_facts_to_learn; false)
end
else
false