--- a/src/HOL/TPTP/MaSh_Eval.thy Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy Sat Dec 15 22:19:14 2012 +0100
@@ -41,7 +41,7 @@
ML {*
if do_it then
- evaluate_mash_suggestions @{context} params (SOME prob_dir)
+ evaluate_mash_suggestions @{context} params (1, NONE) (SOME prob_dir)
(prefix ^ "mash_suggestions") (prefix ^ "mash_eval")
else
()
--- a/src/HOL/TPTP/MaSh_Export.thy Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy Sat Dec 15 22:19:14 2012 +0100
@@ -79,7 +79,7 @@
ML {*
if do_it then
- generate_prover_dependencies @{context} params thys false
+ generate_prover_dependencies @{context} params (1, NONE) thys false
(prefix ^ "mash_prover_dependencies")
else
()
@@ -87,7 +87,7 @@
ML {*
if do_it then
- generate_prover_commands @{context} params thys
+ generate_prover_commands @{context} params (1, NONE) thys
(prefix ^ "mash_prover_commands")
else
()
--- a/src/HOL/TPTP/mash_eval.ML Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Sat Dec 15 22:19:14 2012 +0100
@@ -10,33 +10,41 @@
type params = Sledgehammer_Provers.params
val evaluate_mash_suggestions :
- Proof.context -> params -> string option -> string -> string -> unit
+ Proof.context -> params -> int * int option -> string option -> string
+ -> string -> unit
end;
structure MaSh_Eval : MASH_EVAL =
struct
+open Sledgehammer_Util
open Sledgehammer_Fact
+open Sledgehammer_MePo
open Sledgehammer_MaSh
+open Sledgehammer_Provers
+open Sledgehammer_Isar
val MePoN = "MePo"
val MaShN = "MaSh"
val MeShN = "MeSh"
val IsarN = "Isar"
-fun evaluate_mash_suggestions ctxt params prob_dir_name sugg_file_name
+fun in_range (from, to) j =
+ j >= from andalso (to = NONE orelse j <= the to)
+
+fun evaluate_mash_suggestions ctxt params range prob_dir_name sugg_file_name
report_file_name =
let
val report_path = report_file_name |> Path.explode
val _ = File.write report_path ""
fun print s = (tracing s; File.append report_path (s ^ "\n"))
val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
- Sledgehammer_Isar.default_params ctxt []
+ default_params ctxt []
val prover = hd provers
val slack_max_facts = generous_max_facts (the max_facts)
val sugg_path = sugg_file_name |> Path.explode
val lines = sugg_path |> File.read_lines
- val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+ val css = clasimpset_rule_table_of ctxt
val facts = all_facts ctxt true false Symtab.empty [] [] css
val all_names = build_all_names nickname_of facts
val mepo_ok = Unsynchronized.ref 0
@@ -46,7 +54,7 @@
fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
fun index_string (j, s) = s ^ "@" ^ string_of_int j
fun str_of_res label facts ({outcome, run_time, used_facts, ...}
- : Sledgehammer_Provers.prover_result) =
+ : prover_result) =
let val facts = facts |> map (fn ((name, _), _) => name ()) in
" " ^ label ^ ": " ^
(if is_none outcome then
@@ -66,69 +74,78 @@
|> space_implode " "))
end
fun solve_goal (j, line) =
- let
- val (name, suggs) = extract_query line
- val th =
- case find_first (fn (_, th) => nickname_of th = name) facts of
- SOME (_, th) => th
- | NONE => error ("No fact called \"" ^ name ^ "\".")
- val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
- val isar_deps = isar_dependencies_of all_names th |> these
- val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
- val mepo_facts =
- Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
- slack_max_facts NONE hyp_ts concl_t facts
- |> Sledgehammer_MePo.weight_mepo_facts
- val (mash_facts, mash_unks) =
- find_mash_suggestions slack_max_facts suggs facts [] []
- |>> weight_mash_facts
- val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))]
- val mesh_facts = mesh_facts slack_max_facts mess
- val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts
- (* adapted from "mirabelle_sledgehammer.ML" *)
- fun set_file_name heading (SOME dir) =
- let val prob_prefix = "goal_" ^ string_of_int j ^ "_" ^ heading in
- Config.put Sledgehammer_Provers.dest_dir dir
- #> Config.put Sledgehammer_Provers.problem_prefix
- (prob_prefix ^ "__")
- #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
- end
- | set_file_name _ NONE = I
- fun prove ok heading get facts =
- let
- fun nickify ((_, stature), th) = ((K (nickname_of th), stature), th)
- val facts =
- facts
- |> map get
- |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
- |> take (the max_facts)
- |> map nickify
- val ctxt = ctxt |> set_file_name heading prob_dir_name
- val res as {outcome, ...} =
- run_prover_for_mash ctxt params prover facts goal
- val _ = if is_none outcome then ok := !ok + 1 else ()
- in str_of_res heading facts res end
- val [mepo_s, mash_s, mesh_s, isar_s] =
- [fn () => prove mepo_ok MePoN fst mepo_facts,
- fn () => prove mash_ok MaShN fst mash_facts,
- fn () => prove mesh_ok MeShN I mesh_facts,
- fn () => prove isar_ok IsarN fst isar_facts]
- |> (* Par_List. *) map (fn f => f ())
- in
- ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
- isar_s]
- |> cat_lines |> print
- end
+ if in_range range j then
+ let
+ val (name, suggs) = extract_query line
+ val th =
+ case find_first (fn (_, th) => nickname_of th = name) facts of
+ SOME (_, th) => th
+ | NONE => error ("No fact called \"" ^ name ^ "\".")
+ val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
+ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
+ val isar_deps = isar_dependencies_of all_names th |> these
+ val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
+ val mepo_facts =
+ mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts
+ concl_t facts
+ |> weight_mepo_facts
+ val (mash_facts, mash_unks) =
+ find_mash_suggestions slack_max_facts suggs facts [] []
+ |>> weight_mash_facts
+ val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))]
+ val mesh_facts = mesh_facts slack_max_facts mess
+ val isar_facts =
+ find_suggested_facts (map (rpair 1.0) isar_deps) facts
+ (* adapted from "mirabelle_sledgehammer.ML" *)
+ fun set_file_name heading (SOME dir) =
+ let
+ val prob_prefix =
+ "goal_" ^ string_of_int j ^ "__" ^ escape_meta name ^ "__" ^
+ heading
+ in
+ Config.put dest_dir dir
+ #> Config.put problem_prefix (prob_prefix ^ "__")
+ #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
+ end
+ | set_file_name _ NONE = I
+ fun prove ok heading get facts =
+ let
+ fun nickify ((_, stature), th) =
+ ((K (nickname_of th), stature), th)
+ val facts =
+ facts
+ |> map get
+ |> maybe_instantiate_inducts ctxt hyp_ts concl_t
+ |> take (the max_facts)
+ |> map nickify
+ val ctxt = ctxt |> set_file_name heading prob_dir_name
+ val res as {outcome, ...} =
+ run_prover_for_mash ctxt params prover facts goal
+ val _ = if is_none outcome then ok := !ok + 1 else ()
+ in str_of_res heading facts res end
+ val [mepo_s, mash_s, mesh_s, isar_s] =
+ [fn () => prove mepo_ok MePoN fst mepo_facts,
+ fn () => prove mash_ok MaShN fst mash_facts,
+ fn () => prove mesh_ok MeShN I mesh_facts,
+ fn () => prove isar_ok IsarN fst isar_facts]
+ |> (* Par_List. *) map (fn f => f ())
+ in
+ ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
+ isar_s]
+ |> cat_lines |> print
+ end
+ else
+ ()
fun total_of heading ok n =
" " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
Real.fmt (StringCvt.FIX (SOME 1))
(100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
- val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts
+ val inst_inducts = Config.get ctxt instantiate_inducts
val options =
[prover, string_of_int (the max_facts) ^ " facts",
"slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
- the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
+ the_default "smart" lam_trans,
+ ATP_Util.string_from_time (timeout |> the_default one_year),
"instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
val n = length lines
in
--- a/src/HOL/TPTP/mash_export.ML Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML Sat Dec 15 22:19:14 2012 +0100
@@ -16,11 +16,12 @@
val generate_isar_dependencies :
Proof.context -> theory list -> bool -> string -> unit
val generate_prover_dependencies :
- Proof.context -> params -> theory list -> bool -> string -> unit
+ Proof.context -> params -> int * int option -> theory list -> bool -> string
+ -> unit
val generate_isar_commands :
Proof.context -> string -> theory list -> string -> unit
val generate_prover_commands :
- Proof.context -> params -> theory list -> string -> unit
+ Proof.context -> params -> int * int option -> theory list -> string -> unit
val generate_mepo_suggestions :
Proof.context -> params -> theory list -> int -> string -> unit
end;
@@ -32,6 +33,9 @@
open Sledgehammer_MePo
open Sledgehammer_MaSh
+fun in_range (from, to) j =
+ j >= from andalso (to = NONE orelse j <= the to)
+
fun thy_map_from_facts ths =
ths |> rev
|> map (snd #> `(theory_of_thm #> Context.theory_name))
@@ -108,24 +112,28 @@
| NONE => isar_dependencies_of all_names th)
|> these
-fun generate_isar_or_prover_dependencies ctxt params_opt thys include_thys
+fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
file_name =
let
val path = file_name |> Path.explode
val facts =
all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
val all_names = build_all_names nickname_of facts
- fun do_fact (_, th) =
- let
- val name = nickname_of th
- val deps =
- isar_or_prover_dependencies_of ctxt params_opt facts all_names th NONE
- in escape_meta name ^ ": " ^ escape_metas deps ^ "\n" end
- val lines = Par_List.map do_fact facts
+ fun do_fact (j, (_, th)) =
+ if in_range range j then
+ let
+ val name = nickname_of th
+ val deps =
+ isar_or_prover_dependencies_of ctxt params_opt facts all_names th
+ NONE
+ in escape_meta name ^ ": " ^ escape_metas deps ^ "\n" end
+ else
+ ""
+ val lines = Par_List.map do_fact (tag_list 1 facts)
in File.write_list path lines end
fun generate_isar_dependencies ctxt =
- generate_isar_or_prover_dependencies ctxt NONE
+ generate_isar_or_prover_dependencies ctxt NONE (1, NONE)
fun generate_prover_dependencies ctxt params =
generate_isar_or_prover_dependencies ctxt (SOME params)
@@ -134,38 +142,42 @@
Thm.legacy_get_kind th = "" orelse null isar_deps orelse
is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
-fun generate_isar_or_prover_commands ctxt prover params_opt thys file_name =
+fun generate_isar_or_prover_commands ctxt prover params_opt range thys
+ file_name =
let
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
val path = file_name |> Path.explode
val facts = all_facts ctxt
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
val all_names = build_all_names nickname_of facts
- fun do_fact ((name, ((_, stature), th)), prevs) =
- let
- val feats =
- features_of ctxt prover (theory_of_thm th) stature [prop_of th]
- val isar_deps = isar_dependencies_of all_names th
- val deps =
- isar_or_prover_dependencies_of ctxt params_opt facts all_names th
- (SOME isar_deps)
- val core =
- escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
- encode_features feats
- val query =
- if is_bad_query ctxt ho_atp th (these isar_deps) then ""
- else "? " ^ core ^ "\n"
- val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
- in query ^ update end
+ fun do_fact (j, ((name, ((_, stature), th)), prevs)) =
+ if in_range range j then
+ let
+ val feats =
+ features_of ctxt prover (theory_of_thm th) stature [prop_of th]
+ val isar_deps = isar_dependencies_of all_names th
+ val deps =
+ isar_or_prover_dependencies_of ctxt params_opt facts all_names th
+ (SOME isar_deps)
+ val core =
+ escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
+ encode_features feats
+ val query =
+ if is_bad_query ctxt ho_atp th (these isar_deps) then ""
+ else "? " ^ core ^ "\n"
+ val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
+ in query ^ update end
+ else
+ ""
val thy_map = old_facts |> thy_map_from_facts
val parents = fold (add_thy_parent_facts thy_map) thys []
val new_facts = new_facts |> map (`(nickname_of o snd))
val prevss = fst (split_last (parents :: map (single o fst) new_facts))
- val lines = Par_List.map do_fact (new_facts ~~ prevss)
+ val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss))
in File.write_list path lines end
fun generate_isar_commands ctxt prover =
- generate_isar_or_prover_commands ctxt prover NONE
+ generate_isar_or_prover_commands ctxt prover NONE (1, NONE)
fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) =
generate_isar_or_prover_commands ctxt prover (SOME params)
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Dec 15 22:19:14 2012 +0100
@@ -283,9 +283,7 @@
val monomorphic_term = ATP_Util.monomorphic_term
val specialize_type = ATP_Util.specialize_type
val eta_expand = ATP_Util.eta_expand
-
-fun time_limit NONE = I
- | time_limit (SOME delay) = TimeLimit.timeLimit delay
+val time_limit = Sledgehammer_Util.time_limit
fun DETERM_TIMEOUT delay tac st =
Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Dec 15 22:19:14 2012 +0100
@@ -249,8 +249,6 @@
end)]
end
-val the_timeout = the_default infinite_timeout
-
fun extract_params mode default_params override_params =
let
val raw_params = rev override_params @ rev default_params
@@ -320,11 +318,10 @@
val slice = mode <> Auto_Try andalso lookup_bool "slice"
val minimize =
if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
- val timeout =
- (if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout
+ val timeout = if mode = Auto_Try then NONE else lookup_time "timeout"
val preplay_timeout =
- if mode = Auto_Try then Time.zeroTime
- else lookup_time "preplay_timeout" |> the_timeout
+ if mode = Auto_Try then SOME Time.zeroTime
+ else lookup_time "preplay_timeout"
val expect = lookup_string "expect"
in
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Dec 15 22:19:14 2012 +0100
@@ -818,7 +818,7 @@
if is_smt_prover ctxt prover then
()
else
- launch_thread timeout (fn () =>
+ launch_thread (timeout |> the_default one_day) (fn () =>
let
val thy = Proof_Context.theory_of ctxt
val name = freshish_name ()
@@ -920,7 +920,10 @@
(commit false adds [] []; ([], next_commit_time ()))
else
(adds, next_commit)
- val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
+ val timed_out =
+ case learn_timeout of
+ SOME timeout => Time.> (Timer.checkRealTimer timer, timeout)
+ | NONE => false
in (adds, ([name], n, next_commit, timed_out)) end
val n =
if null new_facts then
@@ -951,7 +954,10 @@
(commit false [] reps flops; ([], [], next_commit_time ()))
else
(reps, flops, next_commit)
- val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
+ val timed_out =
+ case learn_timeout of
+ SOME timeout => Time.> (Timer.checkRealTimer timer, timeout)
+ | NONE => false
in ((reps, flops), (n, next_commit, timed_out)) end
val n =
if not run_prover orelse null old_facts then
@@ -1003,15 +1009,15 @@
val num_facts = length facts
val prover = hd provers
fun learn auto_level run_prover =
- mash_learn_facts ctxt params prover auto_level run_prover infinite_timeout
- facts
+ mash_learn_facts ctxt params prover auto_level run_prover NONE facts
|> Output.urgent_message
in
if run_prover then
("MaShing through " ^ string_of_int num_facts ^ " fact" ^
plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^
- " timeout: " ^ string_from_time timeout ^
- ").\n\nCollecting Isar proofs first..."
+ (case timeout of
+ SOME timeout => " timeout: " ^ string_from_time timeout
+ | NONE => "") ^ ").\n\nCollecting Isar proofs first..."
|> Output.urgent_message;
learn 1 false;
"Now collecting automatic proofs. This may take several hours. You can \
@@ -1048,9 +1054,12 @@
let
fun maybe_learn () =
if learn andalso 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
- launch_thread timeout
+ (timeout = NONE orelse
+ Time.toSeconds (the timeout) >= min_secs_for_learning) then
+ let
+ val timeout = Option.map (time_mult learn_timeout_slack) timeout
+ in
+ launch_thread (timeout |> the_default one_day)
(fn () => (true, mash_learn_facts ctxt params prover 2 false
timeout facts))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Dec 15 22:19:14 2012 +0100
@@ -61,8 +61,12 @@
val _ =
print silent (fn () =>
"Testing " ^ n_facts (map fst facts) ^
- (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
- else "") ^ "...")
+ (if verbose then
+ case timeout of
+ SOME timeout => " (timeout: " ^ string_from_time timeout ^ ")"
+ | _ => ""
+ else
+ "") ^ "...")
val {goal, ...} = Proof.goal state
val facts =
facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
@@ -101,10 +105,11 @@
part of the timeout. *)
val slack_msecs = 200
-fun new_timeout timeout run_time =
- Int.min (Time.toMilliseconds timeout,
- Time.toMilliseconds run_time + slack_msecs)
- |> Time.fromMilliseconds
+fun new_timeout NONE _ = NONE
+ | new_timeout (SOME timeout) run_time =
+ Int.min (Time.toMilliseconds timeout,
+ Time.toMilliseconds run_time + slack_msecs)
+ |> Time.fromMilliseconds |> SOME
(* The linear algorithm usually outperforms the binary algorithm when over 60%
of the facts are actually needed. The binary algorithm is much more
@@ -222,11 +227,12 @@
| {outcome = SOME TimedOut, preplay, ...} =>
(NONE,
(preplay,
- fn _ => "Timeout: You can increase the time limit using the \
- \\"timeout\" option (e.g., \"timeout = " ^
- string_of_int (10 + Time.toMilliseconds timeout div 1000) ^
- "\").",
- ""))
+ fn _ =>
+ "Timeout: You can increase the time limit using the \"timeout\" \
+ \option (e.g., \"timeout = " ^
+ string_of_int (10 + Time.toMilliseconds
+ (timeout |> the_default (seconds 60.0)) div 1000) ^
+ "\").", ""))
| {preplay, message, ...} =>
(NONE, (preplay, prefix "Prover error: " o message, "")))
handle ERROR msg =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Dec 15 22:19:14 2012 +0100
@@ -37,8 +37,8 @@
isar_shrink : real,
slice : bool,
minimize : bool option,
- timeout : Time.time,
- preplay_timeout : Time.time,
+ timeout : Time.time option,
+ preplay_timeout : Time.time option,
expect : string}
type relevance_fudge =
@@ -330,8 +330,8 @@
isar_shrink : real,
slice : bool,
minimize : bool option,
- timeout : Time.time,
- preplay_timeout : Time.time,
+ timeout : Time.time option,
+ preplay_timeout : Time.time option,
expect : string}
type relevance_fudge =
@@ -479,7 +479,7 @@
let
val {context = ctxt, facts, goal} = Proof.goal state
val full_tac = Method.insert_tac facts i THEN tac ctxt i
- in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
+ in time_limit timeout (try (Seq.pull o full_tac)) goal end
fun tac_for_reconstructor (Metis (type_enc, lam_trans)) =
metis_tac [type_enc] lam_trans
@@ -500,39 +500,40 @@
fun play_one_line_proof mode debug verbose timeout pairs state i preferred
reconstrs =
let
- val _ =
- if mode = Minimize andalso Time.> (timeout, Time.zeroTime) then
- Output.urgent_message "Preplaying proof..."
- else
- ()
- val ths = pairs |> sort_wrt (fst o fst) |> map snd
fun get_preferred reconstrs =
if member (op =) reconstrs preferred then preferred
else List.last reconstrs
- fun play [] [] = Failed_to_Play (get_preferred reconstrs)
- | play timed_outs [] =
- Trust_Playable (get_preferred timed_outs, SOME timeout)
- | play timed_out (reconstr :: reconstrs) =
- let
- val _ =
- if verbose then
- "Trying \"" ^ string_for_reconstructor reconstr ^ "\" for " ^
- string_from_time timeout ^ "..."
- |> Output.urgent_message
- else
- ()
- val timer = Timer.startRealTimer ()
- in
- case timed_reconstructor reconstr debug timeout ths state i of
- SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
- | _ => play timed_out reconstrs
- end
- handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
in
- if timeout = Time.zeroTime then
+ if timeout = SOME Time.zeroTime then
Trust_Playable (get_preferred reconstrs, NONE)
else
- play [] reconstrs
+ let
+ val _ =
+ if mode = Minimize then Output.urgent_message "Preplaying proof..."
+ else ()
+ val ths = pairs |> sort_wrt (fst o fst) |> map snd
+ fun play [] [] = Failed_to_Play (get_preferred reconstrs)
+ | play timed_outs [] =
+ Trust_Playable (get_preferred timed_outs, timeout)
+ | play timed_out (reconstr :: reconstrs) =
+ let
+ val _ =
+ if verbose then
+ "Trying \"" ^ string_for_reconstructor reconstr ^ "\"" ^
+ (case timeout of
+ SOME timeout => " for " ^ string_from_time timeout
+ | NONE => "") ^ "..."
+ |> Output.urgent_message
+ else
+ ()
+ val timer = Timer.startRealTimer ()
+ in
+ case timed_reconstructor reconstr debug timeout ths state i of
+ SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
+ | _ => play timed_out reconstrs
+ end
+ handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
+ in play [] reconstrs end
end
@@ -734,20 +735,27 @@
val sound = is_type_enc_sound type_enc
val real_ms = Real.fromInt o Time.toMilliseconds
val slice_timeout =
- ((real_ms time_left
- |> (if slice < num_actual_slices - 1 then
- curry Real.min (time_frac * real_ms timeout)
- else
- I))
- * 0.001) |> seconds
+ case time_left of
+ SOME time_left =>
+ ((real_ms time_left
+ |> (if slice < num_actual_slices - 1 then
+ curry Real.min (time_frac * real_ms (the timeout))
+ else
+ I))
+ * 0.001)
+ |> seconds |> SOME
+ | NONE => NONE
val generous_slice_timeout =
- Time.+ (slice_timeout, atp_timeout_slack)
+ if mode = MaSh then NONE
+ else Option.map (curry Time.+ atp_timeout_slack) slice_timeout
val _ =
if debug then
quote name ^ " slice #" ^ string_of_int (slice + 1) ^
" with " ^ string_of_int num_facts ^ " fact" ^
- plural_s num_facts ^ " for " ^
- string_from_time slice_timeout ^ "..."
+ plural_s num_facts ^
+ (case slice_timeout of
+ SOME timeout => " for " ^ string_from_time timeout
+ | NONE => "") ^ "..."
|> Output.urgent_message
else
()
@@ -778,7 +786,8 @@
fun ord_info () = atp_problem_term_order_info atp_problem
val ord = effective_term_order ctxt name
val full_proof = debug orelse isar_proofs
- val args = arguments ctxt full_proof extra slice_timeout
+ val args = arguments ctxt full_proof extra
+ (slice_timeout |> the_default one_day)
(ord, ord_info, sel_weights)
val command =
"(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
@@ -790,8 +799,8 @@
|> cons ("% " ^ command ^ "\n")
|> File.write_list prob_path
val ((output, run_time), (atp_proof, outcome)) =
- TimeLimit.timeLimit generous_slice_timeout
- Isabelle_System.bash_output command
+ time_limit generous_slice_timeout Isabelle_System.bash_output
+ command
|>> (if overlord then
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
else
@@ -805,7 +814,7 @@
handle UNRECOGNIZED_ATP_PROOF () =>
([], SOME ProofIncomplete)))
handle TimeLimit.TimeOut =>
- (("", slice_timeout), ([], SOME TimedOut))
+ (("", the slice_timeout), ([], SOME TimedOut))
val outcome =
case outcome of
NONE =>
@@ -826,9 +835,13 @@
fun maybe_run_slice slice
(result as (cache, (_, run_time0, _, SOME _))) =
let
- val time_left = Time.- (timeout, Timer.checkRealTimer timer)
+ val time_left =
+ Option.map
+ (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
+ timeout
in
- if Time.<= (time_left, Time.zeroTime) then
+ if time_left <> NONE andalso
+ Time.<= (the time_left, Time.zeroTime) then
result
else
run_slice time_left cache slice
@@ -979,22 +992,25 @@
(repair_monomorph_context max_mono_iters
default_max_mono_iters max_new_mono_instances
default_max_new_mono_instances)
- val ms = timeout |> Time.toMilliseconds
val slice_timeout =
- if slice < max_slices then
- Int.min (ms,
- Int.max (1000 * Config.get ctxt smt_slice_min_secs,
- Real.ceil (Config.get ctxt smt_slice_time_frac
- * Real.fromInt ms)))
- |> Time.fromMilliseconds
+ if slice < max_slices andalso timeout <> NONE then
+ let val ms = timeout |> the |> Time.toMilliseconds in
+ Int.min (ms,
+ Int.max (1000 * Config.get ctxt smt_slice_min_secs,
+ Real.ceil (Config.get ctxt smt_slice_time_frac
+ * Real.fromInt ms)))
+ |> Time.fromMilliseconds |> SOME
+ end
else
timeout
val num_facts = length facts
val _ =
if debug then
quote name ^ " slice " ^ string_of_int slice ^ " with " ^
- string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^
- string_from_time slice_timeout ^ "..."
+ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
+ (case slice_timeout of
+ SOME timeout => " for " ^ string_from_time timeout
+ | NONE => "") ^ "..."
|> Output.urgent_message
else
()
@@ -1004,7 +1020,7 @@
val state_facts = these (try (#facts o Proof.goal) state)
val (outcome, used_facts) =
SMT_Solver.smt_filter_preprocess ctxt state_facts goal facts i
- |> SMT_Solver.smt_filter_apply slice_timeout
+ |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day)
|> (fn {outcome, used_facts} => (outcome, used_facts))
handle exn => if Exn.is_interrupt exn then
reraise exn
@@ -1022,10 +1038,14 @@
| SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
| SOME SMT_Failure.Out_Of_Memory => true
| SOME (SMT_Failure.Other_Failure _) => true
- val timeout = Time.- (timeout, Timer.checkRealTimer timer)
+ val timeout =
+ Option.map
+ (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
+ timeout
in
if too_many_facts_perhaps andalso slice < max_slices andalso
- num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
+ num_facts > 0 andalso
+ (timeout = NONE orelse Time.> (the timeout, Time.zeroTime)) then
let
val new_num_facts =
Real.ceil (Config.get ctxt smt_slice_fact_frac
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sat Dec 15 22:19:14 2012 +0100
@@ -23,7 +23,7 @@
type one_line_params =
play * string * (string * stature) list * minimize_command * int * int
type isar_params =
- bool * bool * Time.time * real * string Symtab.table
+ bool * bool * Time.time option * real * string Symtab.table
* (string * stature) list vector * int Symtab.table * string proof * thm
val smtN : string
@@ -592,7 +592,7 @@
in chain_proof NONE end
type isar_params =
- bool * bool * Time.time * real * string Symtab.table
+ bool * bool * Time.time option * real * string Symtab.table
* (string * stature) list vector * int Symtab.table * string proof * thm
fun isar_proof_text ctxt isar_proofs
@@ -607,7 +607,7 @@
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
else partial_typesN
val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
- val preplay = preplay_timeout <> seconds 0.0
+ val preplay = preplay_timeout <> SOME Time.zeroTime
fun isar_proof_of () =
let
@@ -693,10 +693,12 @@
|> redirect_graph axioms tainted
|> map (do_inf true)
|> append assms
- |> (if not preplay andalso isar_shrink <= 1.0
- then pair (false, (true, seconds 0.0)) #> swap
- else shrink_proof debug ctxt type_enc lam_trans preplay
- preplay_timeout (if isar_proofs then isar_shrink else 1000.0))
+ |> (if not preplay andalso isar_shrink <= 1.0 then
+ pair (false, (true, seconds 0.0)) #> swap
+ else
+ shrink_proof debug ctxt type_enc lam_trans preplay
+ preplay_timeout
+ (if isar_proofs then isar_shrink else 1000.0))
(* |>> reorder_proof_to_minimize_jumps (* ? *) *)
|>> chain_direct_proof
|>> kill_useless_labels_in_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Dec 15 22:19:14 2012 +0100
@@ -68,7 +68,7 @@
{state, goal, subgoal, subgoal_count, facts} name =
let
val ctxt = Proof.context_of state
- val hard_timeout = Time.+ (timeout, timeout)
+ val hard_timeout = time_mult 2.0 (timeout |> the_default one_day)
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, hard_timeout)
val max_facts =
@@ -131,7 +131,7 @@
in (outcome_code, message) end
in
if mode = Auto_Try then
- let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
+ let val (outcome_code, message) = time_limit timeout go () in
(outcome_code,
state
|> outcome_code = someN
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Sat Dec 15 22:19:14 2012 +0100
@@ -9,8 +9,8 @@
sig
type isar_step = Sledgehammer_Proof.isar_step
val shrink_proof :
- bool -> Proof.context -> string -> string -> bool -> Time.time -> real
- -> isar_step list -> isar_step list * (bool * (bool * Time.time))
+ bool -> Proof.context -> string -> string -> bool -> Time.time option
+ -> real -> isar_step list -> isar_step list * (bool * (bool * Time.time))
end
structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK =
@@ -46,7 +46,7 @@
(* Timing *)
fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
-val no_time = (false, seconds 0.0)
+val no_time = (false, Time.zeroTime)
fun take_time timeout tac arg =
let val timing = Timing.start () in
(TimeLimit.timeLimit timeout tac arg;
@@ -59,15 +59,18 @@
fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
isar_shrink proof =
let
+ (* 60 seconds seems like a good interpreation of "no timeout" *)
+ val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
+
(* handle metis preplay fail *)
local
open Unsynchronized
val metis_fail = ref false
in
fun handle_metis_fail try_metis () =
- try_metis () handle _ => (metis_fail := true ; SOME (seconds 0.0))
+ try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime)
fun get_time lazy_time =
- if !metis_fail then SOME (seconds 0.0) else Lazy.force lazy_time
+ if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
val metis_fail = fn () => !metis_fail
end
@@ -120,7 +123,7 @@
|> maps (thms_of_name ctxt)
fun try_metis timeout (succedent, Prove (_, _, t, byline)) =
- if not preplay then (fn () => SOME (seconds 0.0)) else
+ if not preplay then (fn () => SOME Time.zeroTime) else
(case byline of
By_Metis fact_names =>
let
@@ -154,7 +157,7 @@
in
take_time timeout (fn () => goal tac)
end)
- | try_metis _ _ = (fn () => SOME (seconds 0.0) )
+ | try_metis _ _ = (fn () => SOME Time.zeroTime)
val try_metis_quietly = the_default NONE oo try oo try_metis
@@ -195,7 +198,7 @@
NONE => (NONE, metis_time)
| some_t12 =>
(SOME s12, metis_time
- |> replace (seconds 0.0 |> SOME |> Lazy.value) i
+ |> replace (Time.zeroTime |> SOME |> Lazy.value) i
|> replace (Lazy.value some_t12) j)
end))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Dec 15 22:19:14 2012 +0100
@@ -19,6 +19,9 @@
val reserved_isar_keyword_table : unit -> unit Symtab.table
val thms_in_proof : string Symtab.table option -> thm -> string list
val thms_of_name : Proof.context -> string -> thm list
+ val one_day : Time.time
+ val one_year : Time.time
+ val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
end;
@@ -119,6 +122,12 @@
|> Source.exhaust
end
+val one_day = seconds (24.0 * 60.0 * 60.0)
+val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0)
+
+fun time_limit NONE = I
+ | time_limit (SOME delay) = TimeLimit.timeLimit delay
+
fun with_vanilla_print_mode f x =
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
(print_mode_value ())) f x