# 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 \<and> 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;