# HG changeset patch # User wenzelm # Date 1376734433 -7200 # Node ID 0f76e620561f3e2fdc6a10c9525cc7c8cd51f610 # Parent 8dceafa07c4fb959ccb18fa53518db9021ac8612 more direct sledgehammer configuration via mode = Normal_Result and output_result; retain standard sledgehammer parallelization policies; diff -r 8dceafa07c4f -r 0f76e620561f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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")); diff -r 8dceafa07c4f -r 0f76e620561f src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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