# HG changeset patch # User blanchet # Date 1443812792 -7200 # Node ID 150aa3015c478d6435db1e8317619ed71fe696ca # Parent 9a50ea544fd3a708adc122bb03f7b036ae601025 removed legacy asynchronous mode in Sledgehammer diff -r 9a50ea544fd3 -r 150aa3015c47 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 02 21:06:32 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 02 21:06:32 2015 +0200 @@ -117,8 +117,8 @@ end end -fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout, - preplay_timeout, expect, ...}) mode writeln_result only learn +fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout, + expect, ...}) mode writeln_result only learn {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = let val ctxt = Proof.context_of state @@ -214,17 +214,15 @@ if expect = "" orelse outcome_code = expect orelse not (is_prover_installed ctxt name) then () - else if blocking then + else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") - else - warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); in (outcome_code, message) end in if mode = Auto_Try then let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in (outcome_code, if outcome_code = someN then [message ()] else []) end - else if blocking then + else let val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () val outcome = @@ -237,11 +235,6 @@ |> Async_Manager_Legacy.break_into_chunks |> List.app writeln in (outcome_code, []) end - else - (Async_Manager_Legacy.thread SledgehammerN birth_time death_time - (prover_description verbose name num_facts) - ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go); - (unknownN, [])) end val auto_try_max_facts_divisor = 2 (* FUDGE *) @@ -257,14 +250,13 @@ cat_lines (map (fn (filter, facts) => (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss) -fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode - writeln_result i (fact_override as {only, ...}) state = +fun run_sledgehammer (params as {verbose, spy, provers, max_facts, ...}) mode writeln_result i + (fact_override as {only, ...}) state = if null provers then error "No prover is set." else (case subgoal_count state of - 0 => - ((if blocking then error else writeln) "No subgoal!"; (false, (noneN, []))) + 0 => (error "No subgoal!"; (false, (noneN, []))) | n => let val _ = Proof.assert_backward state @@ -278,7 +270,6 @@ val css = clasimpset_rule_table_of ctxt val all_facts = nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t - val _ = () |> not blocking ? kill_provers val _ = (case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") @@ -325,13 +316,13 @@ else (learn chained; provers - |> (if blocking then Par_List.map else map) (launch problem #> fst) + |> Par_List.map (launch problem #> fst) |> max_outcome_code |> rpair []) end in - (if blocking then launch_provers () - else (Future.fork launch_provers; (unknownN, []))) - handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, [])) + launch_provers () + handle TimeLimit.TimeOut => + (print "Sledgehammer ran out of time."; (unknownN, [])) end |> `(fn (outcome_code, _) => outcome_code = someN)) diff -r 9a50ea544fd3 -r 150aa3015c47 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 02 21:06:32 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 02 21:06:32 2015 +0200 @@ -32,10 +32,8 @@ val z3N = "z3" val runN = "run" -val messagesN = "messages" val supported_proversN = "supported_provers" -val kill_allN = "kill_all" -val running_proversN = "running_provers" +val kill_learnersN = "kill_learners" val running_learnersN = "running_learners" val refresh_tptpN = "refresh_tptp" @@ -59,7 +57,6 @@ ("verbose", "false"), ("overlord", "false"), ("spy", "false"), - ("blocking", "false"), ("type_enc", "smart"), ("strict", "false"), ("lam_trans", "smart"), @@ -88,7 +85,6 @@ ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), - ("non_blocking", "blocking"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), @@ -248,8 +244,6 @@ val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" - val blocking = - Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse lookup_bool "blocking" val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd val type_enc = if mode = Auto_Try then @@ -280,8 +274,8 @@ val preplay_timeout = lookup_time "preplay_timeout" val expect = lookup_string "expect" in - {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking, - provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, + {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, + type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, @@ -330,14 +324,10 @@ ignore (run_sledgehammer (get_params Normal thy override_params) Normal writeln_result i fact_override state) end - else if subcommand = messagesN then - messages opt_i else if subcommand = supported_proversN then supported_provers ctxt - else if subcommand = kill_allN then - (kill_provers (); kill_learners ()) - else if subcommand = running_proversN then - running_provers () + else if subcommand = kill_learnersN then + kill_learners () else if subcommand = unlearnN then mash_unlearn () else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse @@ -418,7 +408,6 @@ ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]), ("try0", [try0_arg]), - ("blocking", ["true"]), ("debug", ["false"]), ("verbose", ["false"]), ("overlord", ["false"])]); diff -r 9a50ea544fd3 -r 150aa3015c47 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Oct 02 21:06:32 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Oct 02 21:06:32 2015 +0200 @@ -22,7 +22,6 @@ verbose : bool, overlord : bool, spy : bool, - blocking : bool, provers : string list, type_enc : string option, strict : bool, @@ -73,11 +72,7 @@ ((''a * stature) * 'b) list val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> Proof.context - val supported_provers : Proof.context -> unit - val kill_provers : unit -> unit - val running_provers : unit -> unit - val messages : int option -> unit end; structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER = @@ -111,7 +106,6 @@ verbose : bool, overlord : bool, spy : bool, - blocking : bool, provers : string list, type_enc : string option, strict : bool, @@ -201,8 +195,4 @@ writeln ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".") end -fun kill_provers () = Async_Manager_Legacy.kill_threads SledgehammerN "prover" -fun running_provers () = Async_Manager_Legacy.running_threads SledgehammerN "prover" -val messages = Async_Manager_Legacy.thread_messages SledgehammerN "prover" - end; diff -r 9a50ea544fd3 -r 150aa3015c47 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Oct 02 21:06:32 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Oct 02 21:06:32 2015 +0200 @@ -88,8 +88,8 @@ val facts = facts |> maps (fn (n, ths) => map (pair n) ths) val params = - {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true, - provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, + {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, + type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,