more direct sledgehammer configuration via mode = Normal_Result and output_result;
retain standard sledgehammer parallelization policies;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 17 11:34:50 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 17 12:13:53 2013 +0200
@@ -384,7 +384,7 @@
in
if subcommand = runN then
let val i = the_default 1 opt_i in
- run_sledgehammer (get_params Normal ctxt override_params) Normal i
+ run_sledgehammer (get_params Normal ctxt override_params) Normal NONE i
fact_override (minimize_command override_params i)
state
|> K ()
@@ -489,7 +489,7 @@
val mode = if auto then Auto_Try else Try
val i = 1
in
- run_sledgehammer (get_params mode ctxt []) mode i no_fact_override
+ run_sledgehammer (get_params mode ctxt []) mode NONE i no_fact_override
(minimize_command [] i) state
end
@@ -502,36 +502,23 @@
let
val [provers_arg, timeout_arg, subgoal_arg, isar_proofs_arg] = args;
val ctxt = Proof.context_of state
+ val mode = Normal_Result
- val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt []
+ val {debug, verbose, overlord, isar_proofs, ...} = get_params mode ctxt []
val override_params =
- ([("timeout", [timeout_arg]),
- ("blocking", ["true"])] @
+ ([("timeout", [timeout_arg]), ("blocking", ["true"])] @
(if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg
then [("isar_proofs", [isar_proofs_arg])] else []) @
(if debug then [("debug", ["false"])] else []) @
(if verbose then [("verbose", ["false"])] else []) @
- (if overlord then [("overlord", ["false"])] else []))
+ (if overlord then [("overlord", ["false"])] else []) @
+ (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]))
|> map (normalize_raw_param ctxt)
val i = the_default 1 (Int.fromString subgoal_arg)
-
- val {provers, ...} =
- get_params Normal ctxt
- (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)])
-
- fun run prover =
- let
- val prover_params = ("provers", [prover]) :: override_params
- val sledgehammer_params = get_params Normal ctxt prover_params
- val minimize = minimize_command prover_params i
- val (_, (_, state')) =
- state
- |> Proof.map_context (Config.put sledgehammer_result_request true)
- |> run_sledgehammer sledgehammer_params Try i no_fact_override minimize
- in output_result (Config.get (Proof.context_of state') sledgehammer_result) end
-
- val _ = Par_Exn.release_all (Par_List.map (Exn.interruptible_capture run) provers);
+ val _ =
+ run_sledgehammer (get_params mode ctxt override_params) mode (SOME output_result) i
+ no_fact_override (minimize_command override_params i) state
in () end
| NONE => error "Unknown proof context"));
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Aug 17 11:34:50 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Aug 17 12:13:53 2013 +0200
@@ -19,10 +19,8 @@
val timeoutN : string
val unknownN : string
val string_of_factss : (string * fact list) list -> string
- val sledgehammer_result_request : bool Config.T
- val sledgehammer_result : string Config.T
val run_sledgehammer :
- params -> mode -> int -> fact_override
+ params -> mode -> (string -> unit) option -> int -> fact_override
-> ((string * string list) list -> string -> minimize_command)
-> Proof.state -> bool * (string * Proof.state)
end;
@@ -66,14 +64,9 @@
(if blocking then "."
else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
-val sledgehammer_result_request =
- Config.bool (Config.declare "sledgehammer_result_request" (fn _ => Config.Bool false));
-val sledgehammer_result =
- Config.string (Config.declare "sledgehammer_result" (fn _ => Config.String ""));
-
fun launch_prover (params as {debug, verbose, blocking, max_facts, slice,
timeout, expect, ...})
- mode minimize_command only learn
+ mode output_result minimize_command only learn
{state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
let
val ctxt = Proof.context_of state
@@ -152,19 +145,18 @@
else if blocking then
let
val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
- val state' =
- if Config.get ctxt sledgehammer_result_request then
- state |> Proof.map_context
- (Config.put sledgehammer_result (quote name ^ ": " ^ message ()))
+ val outcome =
+ if outcome_code = someN orelse mode = Normal orelse mode = Normal_Result then
+ quote name ^ ": " ^ message ()
+ else ""
+ val _ =
+ if outcome <> "" andalso mode = Normal_Result andalso is_some output_result then
+ the output_result outcome
else
- ((if outcome_code = someN orelse mode = Normal orelse mode = Normal_Result then
- quote name ^ ": " ^ message ()
- else
- "")
- |> Async_Manager.break_into_chunks
- |> List.app Output.urgent_message;
- state)
- in (outcome_code, state') end
+ outcome
+ |> Async_Manager.break_into_chunks
+ |> List.app Output.urgent_message
+ in (outcome_code, state) end
else
(Async_Manager.thread SledgehammerN birth_time death_time (desc ())
((fn (outcome_code, message) =>
@@ -194,7 +186,7 @@
fun run_sledgehammer (params as {debug, verbose, blocking, provers, max_facts,
slice, ...})
- mode i (fact_override as {only, ...}) minimize_command state =
+ mode output_result i (fact_override as {only, ...}) minimize_command state =
if null provers then
error "No prover is set."
else case subgoal_count state of
@@ -255,11 +247,9 @@
factss = factss}
fun learn prover =
mash_learn_proof ctxt params prover (prop_of goal) all_facts
- val launch = launch_prover params mode minimize_command only learn
+ val launch = launch_prover params mode output_result minimize_command only learn
in
- if mode = Auto_Try orelse
- Config.get (Proof.context_of state) sledgehammer_result_request
- then
+ if mode = Auto_Try then
(unknownN, state)
|> fold (fn prover => fn accum as (outcome_code, _) =>
if outcome_code = someN then accum