# HG changeset patch
# User desharna
# Date 1752221521 -7200
# Node ID 5e9c9f2c2cd847b55daaefa246f078da03365c86
# Parent  7ddae44464d41ac9c25046b06138bde8952d7a00
added option `-S` to Mirabelle to specify the subgoal classes to consider

diff -r 7ddae44464d4 -r 5e9c9f2c2cd8 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Tue Jul 08 19:13:44 2025 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Fri Jul 11 10:12:01 2025 +0200
@@ -185,8 +185,6 @@
 
 (* presentation hook *)
 
-val whitelist = ["apply", "by", "proof", "unfolding", "using"];
-
 val _ =
   Build.add_hook (fn qualifier => fn loaded_theories =>
     let
@@ -209,6 +207,8 @@
           val mirabelle_output_dir = Options.default_string \<^system_option>\<open>mirabelle_output_dir\<close>;
           val mirabelle_parallel_group_size = Options.default_int \<^system_option>\<open>mirabelle_parallel_group_size\<close>;
           val check_theory = check_theories (space_explode "," mirabelle_theories);
+          val mirabelle_subgoals = Options.default_string \<^system_option>\<open>mirabelle_subgoals\<close>;
+          val considered_subgoals = space_explode "," mirabelle_subgoals;
 
           fun parallel_app (f : 'a -> unit) (xs : 'a list) : unit =
             chop_groups mirabelle_parallel_group_size xs
@@ -225,7 +225,7 @@
                 in
                   if Context.proper_subthy (\<^theory>, thy) andalso
                     can (Proof.assert_backward o Toplevel.proof_of) st andalso
-                    member (op =) whitelist name andalso check_thy pos
+                    member (op =) considered_subgoals name andalso check_thy pos
                   then SOME {theory_index = thy_index, name = name, pos = pos,
                     pre = Toplevel.proof_of st, post = st'}
                   else NONE
diff -r 7ddae44464d4 -r 5e9c9f2c2cd8 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Tue Jul 08 19:13:44 2025 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Jul 11 10:12:01 2025 +0200
@@ -113,6 +113,7 @@
       val mirabelle_timeout = options.check_name("mirabelle_timeout")
       val mirabelle_output_dir = options.check_name("mirabelle_output_dir")
       val mirabelle_parallel_group_size = options.check_name("mirabelle_parallel_group_size")
+      val mirabelle_subgoals = options.check_name("mirabelle_subgoals")
 
       var actions: List[String] = Nil
       var base_sessions: List[String] = Nil
@@ -137,6 +138,7 @@
     -D DIR       include session directory and select its sessions
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -O DIR       """ + mirabelle_output_dir.description + " (default: " + mirabelle_output_dir.default_value + """)
+    -S SUBGOAL   """ + mirabelle_subgoals.description + " (default: " + mirabelle_subgoals.default_value + """)
     -T THEORY    theory restriction: NAME or NAME[FIRST_LINE:LAST_LINE]
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
@@ -171,6 +173,7 @@
         "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
         "N" -> (_ => numa_shuffling = true),
         "O:" -> (arg => output_dir = Path.explode(arg)),
+        "S:" -> (arg => options = options + ("mirabelle_subgoals=" + arg)),
         "T:" -> (arg => theories = theories ::: List(arg)),
         "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
         "a" -> (_ => all_sessions = true),
diff -r 7ddae44464d4 -r 5e9c9f2c2cd8 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Tue Jul 08 19:13:44 2025 +0200
+++ b/src/HOL/Tools/etc/options	Fri Jul 11 10:12:01 2025 +0200
@@ -76,3 +76,6 @@
 
 option mirabelle_theories : string = ""
   -- "Mirabelle theories (names with optional line range, separated by commas)"
+
+option mirabelle_subgoals : string = "apply,by,proof,unfolding,using"
+  -- "comma-separated list of subgoal classes to consider"