--- a/src/Doc/Sledgehammer/document/root.tex Mon Jan 31 16:09:23 2022 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Jan 31 16:09:23 2022 +0100
@@ -1121,7 +1121,8 @@
\textit{overlord} (\S\ref{mode-of-operation}).}
\opdefault{max\_proofs}{int}{\upshape 4}
-Specifies the maximum number of proofs to display before stopping.
+Specifies the maximum number of proofs to display before stopping. This is a
+soft limit.
\opsmart{isar\_proofs}{no\_isar\_proofs}
Specifies whether Isar proofs should be output in addition to one-line proofs.
--- a/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100
@@ -37,7 +37,7 @@
(*
lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x"
- sledgehammer [slices = 4]
+ sledgehammer [max_proofs = 3]
oops
*)
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
@@ -443,12 +443,7 @@
val term_order = AList.lookup (op =) arguments term_orderK
val proof_method_from_msg = proof_method_from_msg arguments
- (* Parse Sledgehammer parameters *)
val params = Sledgehammer_Commands.default_params \<^theory> arguments
- |> (fn (params as {provers, ...}) =>
- (case provers of
- prover :: _ => Sledgehammer_Prover.set_params_provers params [prover]
- | _ => error "sledgehammer action requires one and only one prover"))
val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
@@ -316,7 +316,8 @@
translate prover_slices schedule
end
-fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, slices, ...})
+fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, max_proofs,
+ slices, ...})
mode writeln_result i (fact_override as {only, ...}) state =
if null provers then
error "No prover is set"
@@ -328,12 +329,12 @@
val _ = Proof.assert_backward state
val print = if mode = Normal andalso is_none writeln_result then writeln else K ()
- val proof_found = Synchronized.var "proof_found" false
+ val found_proofs = Synchronized.var "found_proofs" 0
fun found_proof prover_name =
if mode = Normal then
-(* ### Synchronized.change_result proof_found (rpair true) *)
- (writeln_result |> the_default writeln) (prover_name ^ " found a proof...")
+ (Synchronized.change found_proofs (fn n => n + 1);
+ (writeln_result |> the_default writeln) (prover_name ^ " found a proof..."))
else
()
@@ -406,7 +407,12 @@
prover_slices
else
(learn chained_thms;
- Par_List.map (fn (prover, slice) => launch problem slice prover) prover_slices
+ Par_List.map (fn (prover, slice) =>
+ if Synchronized.value found_proofs < max_proofs then
+ launch problem slice prover
+ else
+ (SH_Unknown, ""))
+ prover_slices
|> max_outcome)
end
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jan 31 16:09:23 2022 +0100
@@ -63,6 +63,7 @@
("fact_thresholds", "0.45 0.85"),
("max_mono_iters", "smart"),
("max_new_mono_instances", "smart"),
+ ("max_proofs", "4"),
("isar_proofs", "smart"),
("compress", "smart"),
("try0", "true"),
@@ -259,6 +260,7 @@
val max_mono_iters = lookup_option lookup_int "max_mono_iters"
val max_new_mono_instances =
lookup_option lookup_int "max_new_mono_instances"
+ val max_proofs = lookup_int "max_proofs"
val isar_proofs = lookup_option lookup_bool "isar_proofs"
val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
val try0 = lookup_bool "try0"
@@ -274,9 +276,9 @@
uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
induction_rules = induction_rules, 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, compress = compress, try0 = try0, smt_proofs = smt_proofs,
- minimize = minimize, slices = slices, timeout = timeout, preplay_timeout = preplay_timeout,
- expect = expect}
+ max_proofs = max_proofs, isar_proofs = isar_proofs, compress = compress, try0 = try0,
+ smt_proofs = smt_proofs, minimize = minimize, slices = slices, timeout = timeout,
+ preplay_timeout = preplay_timeout, expect = expect}
end
fun get_params mode = extract_params mode o default_raw_params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 16:09:23 2022 +0100
@@ -40,6 +40,7 @@
fact_thresholds : real * real,
max_mono_iters : int option,
max_new_mono_instances : int option,
+ max_proofs : int,
isar_proofs : bool option,
compress : real option,
try0 : bool,
@@ -51,7 +52,6 @@
expect : string}
val string_of_params : params -> string
- val set_params_provers : params -> string list -> params
val slice_timeout : int -> Time.time -> Time.time
type prover_problem =
@@ -141,6 +141,7 @@
fact_thresholds : real * real,
max_mono_iters : int option,
max_new_mono_instances : int option,
+ max_proofs : int,
isar_proofs : bool option,
compress : real option,
try0 : bool,
@@ -158,33 +159,6 @@
induction_rules = Exclude ?
filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false)
-fun set_params_provers params provers =
- {debug = #debug params,
- verbose = #verbose params,
- overlord = #overlord params,
- spy = #spy params,
- provers = provers,
- type_enc = #type_enc params,
- strict = #strict params,
- lam_trans = #lam_trans params,
- uncurried_aliases = #uncurried_aliases params,
- learn = #learn params,
- fact_filter = #fact_filter params,
- induction_rules = #induction_rules params,
- max_facts = #max_facts params,
- fact_thresholds = #fact_thresholds params,
- max_mono_iters = #max_mono_iters params,
- max_new_mono_instances = #max_new_mono_instances params,
- isar_proofs = #isar_proofs params,
- compress = #compress params,
- try0 = #try0 params,
- smt_proofs = #smt_proofs params,
- minimize = #minimize params,
- slices = #slices params,
- timeout = #timeout params,
- preplay_timeout = #preplay_timeout params,
- expect = #expect params}
-
fun slice_timeout slices timeout =
Time.toReal timeout * Real.fromInt (Multithreading.max_threads ()) / Real.fromInt slices
|> seconds
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 16:09:23 2022 +0100
@@ -94,9 +94,10 @@
uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
induction_rules = induction_rules, 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, isar_proofs = isar_proofs,
- compress = compress, try0 = try0, smt_proofs = smt_proofs, minimize = minimize,
- slices = 1, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
+ max_new_mono_instances = max_new_mono_instances, max_proofs = 1,
+ isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
+ minimize = minimize, slices = 1, timeout = timeout, preplay_timeout = preplay_timeout,
+ expect = ""}
val problem =
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
factss = [("", facts)], found_proof = K ()}