# HG changeset patch
# User blanchet
# Date 1643641763 -3600
# Node ID 8d08bc7e8f984c79ab1d75ded1009daf7aaa9736
# Parent  ae4dc5ac983f4bf42be8330971a974640e8caf81
tweak padding of prover slice schedule to include all provers

diff -r ae4dc5ac983f -r 8d08bc7e8f98 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
@@ -36,6 +36,15 @@
 ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
 
 (*
+lemma "1 + 1 = 2"
+  sledgehammer [slices = 40, max_proofs = 40]
+
+lemma "1 + 1 = 2"
+  sledgehammer [verbose, slices = 4]
+  oops
+*)
+
+(*
 lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x"
   sledgehammer [max_proofs = 3]
   oops
diff -r ae4dc5ac983f -r 8d08bc7e8f98 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
@@ -272,7 +272,8 @@
 fun schedule_of_provers provers num_slices =
   let
     val num_default_slices = length default_slice_schedule
-    val unknown_provers = filter_out (member (op =) default_slice_schedule) provers
+    val (known_provers, unknown_provers) =
+      List.partition (member (op =) default_slice_schedule) provers
 
     fun round_robin _ [] = []
       | round_robin 0 _ = []
@@ -281,7 +282,8 @@
     if num_slices <= num_default_slices then
       take num_slices default_slice_schedule
     else
-      default_slice_schedule @ round_robin (num_slices - num_default_slices) unknown_provers
+      default_slice_schedule
+      @ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers)
   end
 
 fun prover_slices_of_schedule ctxt schedule =