# HG changeset patch # User blanchet # Date 1643641763 -3600 # Node ID 919fb49ba201837f3fd4294fea6e93630510794a # Parent dc6769b86fd67daa9d7975f4ba70ef454cf3cc80 document new option 'max_proofs' diff -r dc6769b86fd6 -r 919fb49ba201 src/Doc/Sledgehammer/document/root.tex --- 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 @@ -1120,6 +1120,9 @@ {\small See also \textit{spy} (\S\ref{mode-of-operation}) and \textit{overlord} (\S\ref{mode-of-operation}).} +\opdefault{max\_proofs}{int}{\upshape 4} +Specifies the maximum number of proofs to display before stopping. + \opsmart{isar\_proofs}{no\_isar\_proofs} Specifies whether Isar proofs should be output in addition to one-line proofs. The construction of Isar proof is still experimental and may sometimes fail; diff -r dc6769b86fd6 -r 919fb49ba201 src/HOL/Sledgehammer.thy --- 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,8 @@ (* lemma "1 + 1 = 2 \ 0 + (x::nat) = x" - sledgehammer + sledgehammer [slices = 4] + oops *) (* diff -r dc6769b86fd6 -r 919fb49ba201 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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,8 +316,8 @@ translate prover_slices schedule end -fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, ...}) mode - writeln_result i (fact_override as {only, ...}) state = +fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, slices, ...}) + mode writeln_result i (fact_override as {only, ...}) state = if null provers then error "No prover is set" else @@ -328,12 +328,14 @@ val _ = Proof.assert_backward state val print = if mode = Normal andalso is_none writeln_result then writeln else K () - val found_proof = - fn prover_name => - if mode = Normal then - (writeln_result |> the_default writeln) (prover_name ^ " found a proof...") - else - () + val proof_found = Synchronized.var "proof_found" false + + 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...") + else + () val ctxt = Proof.context_of state val inst_inducts = induction_rules = SOME Instantiate @@ -393,9 +395,7 @@ if mode = Auto_Try then provers else - let val num_slices = 50 (* FIXME *) in - schedule_of_provers provers num_slices - end + schedule_of_provers provers slices val prover_slices = prover_slices_of_schedule ctxt schedule in if mode = Auto_Try then @@ -415,8 +415,7 @@ |> `(fn (outcome, _) => (case outcome of SH_Some _ => (print "QED"; true) - | SH_Timeout => (print "Timed out"; false) - | _ => (print "Done"; false))) + | _ => (print "Sorry"; false))) end) end;