--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Wed Aug 04 08:23:12 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Wed Aug 04 08:25:52 2021 +0200
@@ -200,18 +200,21 @@
end;
(* initialize actions *)
- val contexts = actions |> map_index (fn (n, (name, args)) =>
- let
- val make_action = the (get_action name);
- val action_subdir = string_of_int n ^ "." ^ name
- val output_dir =
- Path.append (Path.explode mirabelle_output_dir) (Path.basic action_subdir)
- val context =
- {index = n, name = name, arguments = args, timeout = mirabelle_timeout,
- output_dir = output_dir};
- in
- (make_action context, context)
- end);
+ val contexts =
+ let val padding = ceil (Math.log10 (real (length actions))) in
+ actions |> map_index (fn (n, (name, args)) =>
+ let
+ val make_action = the (get_action name);
+ val action_subdir = StringCvt.padLeft #"0" padding (string_of_int n) ^ "." ^ name;
+ val output_dir =
+ Path.append (Path.explode mirabelle_output_dir) (Path.basic action_subdir);
+ val context =
+ {index = n, name = name, arguments = args, timeout = mirabelle_timeout,
+ output_dir = output_dir};
+ in
+ (make_action context, context)
+ end)
+ end;
in
(* run actions on all relevant goals *)
loaded_theories