# HG changeset patch
# User wenzelm
# Date 1507993185 -7200
# Node ID f6676691ef8afd01f9ead843713b043032e96501
# Parent  54ae2cc05325be59ee74d837f4424070f5d8a5e6
partition AFP sessions according to structure, which happens to cut it roughly into equal parts;

diff -r 54ae2cc05325 -r f6676691ef8a src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Sat Oct 14 15:44:21 2017 +0200
+++ b/src/Pure/Admin/afp.scala	Sat Oct 14 16:59:45 2017 +0200
@@ -81,4 +81,17 @@
   }
  }"""
     }).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 (isolated_sessions, connected_sessions) = graph.keys.partition(graph.is_isolated(_))
+        if (n == 1) isolated_sessions else connected_sessions
+      case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
+    }
 }
diff -r 54ae2cc05325 -r f6676691ef8a src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Oct 14 15:44:21 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Oct 14 16:59:45 2017 +0200
@@ -102,10 +102,12 @@
   private val default_isabelle_identifier = "build_history"
 
   def build_history(
+    options: Options,
     root: Path,
     progress: Progress = No_Progress,
     rev: String = default_rev,
     afp_rev: Option[String] = None,
+    afp_partition: Int = 0,
     isabelle_identifier: String = default_isabelle_identifier,
     components_base: String = "",
     fresh: Boolean = false,
@@ -153,15 +155,22 @@
     }
 
     val isabelle_version = checkout(root, rev)
-    val afp_version = afp_rev.map(checkout(root + Path.explode("AFP"), _))
+
+    val afp_repos = root + Path.explode("AFP")
+    val afp_version = afp_rev.map(checkout(afp_repos, _))
+
+    val (afp_build_options, afp_build_args) =
+      if (afp_rev.isEmpty) (Nil, Nil)
+      else {
+        val afp = AFP.init(options, afp_repos)
+        (List("-d", "~~/AFP/thys"), afp.partition(afp_partition))
+      }
 
 
     /* main */
 
     val other_isabelle = new Other_Isabelle(progress, root, isabelle_identifier)
 
-    val afp_build_args = if (afp_rev.isDefined) List("-d", "~~/AFP/thys") else Nil
-
     val build_host = Isabelle_System.hostname()
     val build_history_date = Date.now()
     val build_group_id = build_host + ":" + build_history_date.time.ms
@@ -214,7 +223,8 @@
         Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
 
       val build_start = Date.now()
-      val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
+      val build_args1 =
+        List("-v", "-j" + processes) ::: afp_build_options ::: build_args ::: afp_build_args
       val build_result =
         (new Other_Isabelle(build_out_progress, root, isabelle_identifier))(
           "build " + Bash.strings(build_args1), redirect = true, echo = true, strict = false)
@@ -335,6 +345,7 @@
       var max_heap: Option[Int] = None
       var multicore_list = List(default_multicore)
       var isabelle_identifier = default_isabelle_identifier
+      var afp_partition = 0
       var more_settings: List[String] = Nil
       var fresh = false
       var init_settings: List[String] = Nil
@@ -357,6 +368,7 @@
       default_heap * 2 + """ for x86_64)
     -M MULTICORE multicore configurations (see below)
     -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
+    -P NUMBER    AFP partition number (0, 1, 2, default: 0=unrestricted)
     -U SIZE      maximal ML heap in MB (default: unbounded)
     -e TEXT      additional text for generated etc/settings
     -f           fresh build of Isabelle/Scala components (recommended)
@@ -381,6 +393,7 @@
         "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
         "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse(_))),
         "N:" -> (arg => isabelle_identifier = arg),
+        "P:" -> (arg => afp_partition = Value.Int.parse(arg)),
         "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
         "e:" -> (arg => more_settings = more_settings ::: List(arg)),
         "f" -> (_ => fresh = true),
@@ -408,10 +421,10 @@
       val progress = new Console_Progress(stderr = true)
 
       val results =
-        build_history(root, progress = progress, rev = rev, afp_rev = afp_rev,
-          isabelle_identifier = isabelle_identifier, components_base = components_base,
-          fresh = fresh, nonfree = nonfree, multicore_base = multicore_base,
-          multicore_list = multicore_list, arch_64 = arch_64,
+        build_history(Options.init(), root, progress = progress, rev = rev, afp_rev = afp_rev,
+          afp_partition = afp_partition, isabelle_identifier = isabelle_identifier,
+          components_base = components_base, fresh = fresh, nonfree = nonfree,
+          multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
           heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
           max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
           verbose = verbose, build_tags = build_tags, build_args = build_args)
diff -r 54ae2cc05325 -r f6676691ef8a src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 14 15:44:21 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 14 16:59:45 2017 +0200
@@ -58,7 +58,7 @@
             File.standard_path(isabelle_repos), isabelle_repos_test)
         for {
           (result, log_path) <-
-            Build_History.build_history(isabelle_repos_test,
+            Build_History.build_history(logger.options, isabelle_repos_test,
               rev = "build_history_base", fresh = true, build_args = List("HOL"))
         } {
           result.check