# HG changeset patch
# User desharna
# Date 1623505045 -7200
# Node ID adb34395b622183206f97e8ec185dd79ff915e7a
# Parent  bb277f37c34ae0157de523ad6a152809f82c368c
added support for unbounded max calls to Mirabelle

diff -r bb277f37c34a -r adb34395b622 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Sat Jun 12 12:39:33 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Sat Jun 12 15:37:25 2021 +0200
@@ -209,7 +209,7 @@
           |> map_index I
           |> maps (fn (n, command) =>
             let val (m, k) = Integer.div_mod (n + 1) mirabelle_stride in
-              if k = 0 andalso m <= mirabelle_max_calls then
+              if k = 0 andalso (mirabelle_max_calls <= 0 orelse m <= mirabelle_max_calls) then
                 map (fn context => (context, command)) contexts
               else
                 []
diff -r bb277f37c34a -r adb34395b622 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Sat Jun 12 12:39:33 2021 +0200
+++ b/src/HOL/Tools/etc/options	Sat Jun 12 15:37:25 2021 +0200
@@ -56,8 +56,8 @@
 option mirabelle_stride : int = 1
   -- "default stride for running Mirabelle actions on every nth goal"
 
-option mirabelle_max_calls : int = 10000000
-  -- "default max. no. of calls to each Mirabelle action"
+option mirabelle_max_calls : int = 0
+  -- "default max. no. of calls to each Mirabelle action (0: unbounded)"
 
 option mirabelle_actions : string = ""
   -- "Mirabelle actions (outer syntax, separated by semicolons)"