# 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