discontinue odd AFP partitioning: let Build_Cluster / Build_Engine do the job;

--- a/src/Pure/Admin/afp.scala	Tue Aug 29 20:14:44 2023 +0200
+++ b/src/Pure/Admin/afp.scala	Tue Aug 29 20:19:57 2023 +0200
@@ -21,8 +21,6 @@
 
   val chapter: String = "AFP"
 
-  val force_partition1: List[String] = List("Category3", "HOL-ODE")
-
   val BASE: Path = Path.explode("$AFP_BASE")
 
   def main_dir(base_dir: Path = BASE): Path = base_dir + Path.explode("thys")
@@ -207,19 +205,4 @@
   }
  }"""
     }).mkString("[", ", ", "\n]\n")
-
-
-  /* partition sessions */
-
-  def partition(n: Int): List[String] =
-    n match {
-      case 0 => Nil
-      case 1 | 2 =>
-        val graph = sessions_structure.build_graph.restrict(sessions.toSet)
-        val force_part1 =
-          graph.all_preds(graph.all_succs(AFP.force_partition1.filter(graph.defined))).toSet
-        val (part1, part2) = graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
-        if (n == 1) part1 else part2
-      case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
-    }
 }

--- a/src/Pure/Admin/build_history.scala	Tue Aug 29 20:14:44 2023 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Aug 29 20:19:57 2023 +0200
@@ -112,7 +112,6 @@
     root: Path,
     progress: Progress = new Progress,
     afp: Boolean = false,
-    afp_partition: Int = 0,
     isabelle_identifier: String = default_isabelle_identifier,
     ml_statistics_step: Int = 1,
     component_repository: String = Components.static_component_repository,
@@ -167,22 +166,9 @@
     }
 
     val isabelle_directory = directory(root)
-    val afp_directory = if (afp) Some(directory(root + Path.explode("AFP"))) else None
-
-    val (afp_build_args, afp_sessions) =
-      if (afp_directory.isEmpty) (Nil, Nil)
-      else {
-        val (opt, sessions) = {
-          if (afp_partition == 0) ("-d", Nil)
-          else {
-            try {
-              val afp_info = AFP.init(options, base_dir = afp_directory.get.root)
-              ("-d", afp_info.partition(afp_partition))
-            } catch { case ERROR(_) => ("-D", Nil) }
-          }
-        }
-        (List(opt, "~~/AFP/thys"), sessions)
-      }
+    val (afp_directory, afp_build_args) =
+      if (afp) (Some(directory(root + Path.explode("AFP"))), List("-d", "~~/AFP/thys"))
+      else (None, Nil)
 
 
     /* main */
@@ -266,7 +252,7 @@
       val build_result =
         Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
           progress = build_out_progress)
-        .bash("bin/isabelle build " + Bash.strings(build_args1 ::: afp_sessions),
+        .bash("bin/isabelle build " + Bash.strings(build_args1),
           redirect = true, echo = true, strict = false)
 
       val build_end = Date.now()
@@ -424,7 +410,6 @@
       var multicore_list = List(default_multicore)
       var isabelle_identifier = default_isabelle_identifier
       var clean_platforms: Option[List[Platform.Family]] = None
-      var afp_partition = 0
       var clean_archives = false
       var component_repository = Components.static_component_repository
       var arch_apple = false
@@ -453,7 +438,6 @@
     -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
     -O PLATFORMS clean resolved components, retaining only the given list
                  platform families (separated by commas; default: do nothing)
-    -P NUMBER    AFP partition number (0, 1, 2, default: 0=unrestricted)
     -Q           clean archives of downloaded components
     -R URL       remote repository for Isabelle components (default: """ +
       Components.static_component_repository + """)
@@ -485,7 +469,6 @@
         "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)),
         "N:" -> (arg => isabelle_identifier = arg),
         "O:" -> (arg => clean_platforms = Some(space_explode(',',arg).map(Platform.Family.parse))),
-        "P:" -> (arg => afp_partition = Value.Int.parse(arg)),
         "Q" -> (_ => clean_archives = true),
         "R:" -> (arg => component_repository = arg),
         "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
@@ -516,8 +499,7 @@
       val progress = new Console_Progress(stderr = true)
 
       val results =
-        local_build(Options.init(), root, progress = progress,
-          afp = afp, afp_partition = afp_partition,
+        local_build(Options.init(), root, progress = progress, afp = afp,
           isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
           component_repository = component_repository, components_base = components_base,
           clean_platforms = clean_platforms, clean_archives = clean_archives,