--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Jan 05 23:03:07 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Jan 06 10:02:34 2013 +0100
@@ -119,7 +119,7 @@
val params_for_minimize =
["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
"uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
- "isar_proofs", "isar_shrink", "timeout", "preplay_timeout"]
+ "learn", "isar_proofs", "isar_shrink", "timeout", "preplay_timeout"]
val property_dependent_params = ["provers", "timeout"]
@@ -345,6 +345,11 @@
member (op =) params_for_minimize name
fun string_for_raw_param (key, values) =
key ^ (case implode_param values of "" => "" | value => " = " ^ value)
+fun nice_string_for_raw_param (p as (key, ["false"])) =
+ (case AList.find (op =) negated_alias_params key of
+ [neg] => neg
+ | _ => string_for_raw_param p)
+ | nice_string_for_raw_param p = string_for_raw_param p
fun minimize_command override_params i more_override_params prover_name
fact_names =
@@ -354,7 +359,7 @@
|> filter_out (AList.defined (op =) more_override_params o fst)) @
more_override_params
|> filter is_raw_param_relevant_for_minimize
- |> map string_for_raw_param
+ |> map nice_string_for_raw_param
|> (if prover_name = default_minimize_prover then I else cons prover_name)
|> space_implode ", "
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Jan 05 23:03:07 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jan 06 10:02:34 2013 +0100
@@ -152,13 +152,13 @@
"\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^
File.shell_path (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^
" >& " ^ err_file
- |> tap (fn _ => trace_msg ctxt (fn () =>
- case try File.read (Path.explode err_file) of
- NONE => "Done"
- | SOME "" => "Done"
- | SOME s => "Error: " ^ elide_string 1000 s))
fun run_on () =
- (Isabelle_System.bash command;
+ (Isabelle_System.bash command
+ |> tap (fn _ => trace_msg ctxt (fn () =>
+ case try File.read (Path.explode err_file) of
+ NONE => "Done"
+ | SOME "" => "Done"
+ | SOME s => "Error: " ^ elide_string 1000 s));
read_suggs (fn () => try File.read_lines sugg_path |> these))
fun clean_up () =
if overlord then ()
@@ -866,7 +866,7 @@
" proofs to learn." ^
(if auto_level = 0 andalso not run_prover then
"\n\nHint: Try " ^ sendback learn_proverN ^
- " to learn from automatic provers."
+ " to learn from an automatic prover."
else
"")
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Jan 05 23:03:07 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Jan 06 10:02:34 2013 +0100
@@ -68,7 +68,7 @@
{state, goal, subgoal, subgoal_count, facts} name =
let
val ctxt = Proof.context_of state
- val hard_timeout = time_mult 2.0 (timeout |> the_default one_day)
+ val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, hard_timeout)
val max_facts =