--- 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))
--- 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"])]);
--- 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;
--- 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,