partition AFP sessions according to structure, which happens to cut it roughly into equal parts;
authorwenzelm
Sat Oct 14 16:59:45 2017 +0200 (22 months ago)
changeset 66861f6676691ef8a
parent 66860 54ae2cc05325
child 66862 136793b73c7c
partition AFP sessions according to structure, which happens to cut it roughly into equal parts;
src/Pure/Admin/afp.scala
src/Pure/Admin/build_history.scala
src/Pure/Admin/isabelle_cronjob.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Sat Oct 14 15:44:21 2017 +0200
     1.2 +++ b/src/Pure/Admin/afp.scala	Sat Oct 14 16:59:45 2017 +0200
     1.3 @@ -81,4 +81,17 @@
     1.4    }
     1.5   }"""
     1.6      }).mkString("[", ", ", "\n]\n")
     1.7 +
     1.8 +
     1.9 +  /* partition sessions */
    1.10 +
    1.11 +  def partition(n: Int): List[String] =
    1.12 +    n match {
    1.13 +      case 0 => Nil
    1.14 +      case 1 | 2 =>
    1.15 +        val graph = sessions_structure.build_graph.restrict(sessions.toSet)
    1.16 +        val (isolated_sessions, connected_sessions) = graph.keys.partition(graph.is_isolated(_))
    1.17 +        if (n == 1) isolated_sessions else connected_sessions
    1.18 +      case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
    1.19 +    }
    1.20  }
     2.1 --- a/src/Pure/Admin/build_history.scala	Sat Oct 14 15:44:21 2017 +0200
     2.2 +++ b/src/Pure/Admin/build_history.scala	Sat Oct 14 16:59:45 2017 +0200
     2.3 @@ -102,10 +102,12 @@
     2.4    private val default_isabelle_identifier = "build_history"
     2.5  
     2.6    def build_history(
     2.7 +    options: Options,
     2.8      root: Path,
     2.9      progress: Progress = No_Progress,
    2.10      rev: String = default_rev,
    2.11      afp_rev: Option[String] = None,
    2.12 +    afp_partition: Int = 0,
    2.13      isabelle_identifier: String = default_isabelle_identifier,
    2.14      components_base: String = "",
    2.15      fresh: Boolean = false,
    2.16 @@ -153,15 +155,22 @@
    2.17      }
    2.18  
    2.19      val isabelle_version = checkout(root, rev)
    2.20 -    val afp_version = afp_rev.map(checkout(root + Path.explode("AFP"), _))
    2.21 +
    2.22 +    val afp_repos = root + Path.explode("AFP")
    2.23 +    val afp_version = afp_rev.map(checkout(afp_repos, _))
    2.24 +
    2.25 +    val (afp_build_options, afp_build_args) =
    2.26 +      if (afp_rev.isEmpty) (Nil, Nil)
    2.27 +      else {
    2.28 +        val afp = AFP.init(options, afp_repos)
    2.29 +        (List("-d", "~~/AFP/thys"), afp.partition(afp_partition))
    2.30 +      }
    2.31  
    2.32  
    2.33      /* main */
    2.34  
    2.35      val other_isabelle = new Other_Isabelle(progress, root, isabelle_identifier)
    2.36  
    2.37 -    val afp_build_args = if (afp_rev.isDefined) List("-d", "~~/AFP/thys") else Nil
    2.38 -
    2.39      val build_host = Isabelle_System.hostname()
    2.40      val build_history_date = Date.now()
    2.41      val build_group_id = build_host + ":" + build_history_date.time.ms
    2.42 @@ -214,7 +223,8 @@
    2.43          Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
    2.44  
    2.45        val build_start = Date.now()
    2.46 -      val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
    2.47 +      val build_args1 =
    2.48 +        List("-v", "-j" + processes) ::: afp_build_options ::: build_args ::: afp_build_args
    2.49        val build_result =
    2.50          (new Other_Isabelle(build_out_progress, root, isabelle_identifier))(
    2.51            "build " + Bash.strings(build_args1), redirect = true, echo = true, strict = false)
    2.52 @@ -335,6 +345,7 @@
    2.53        var max_heap: Option[Int] = None
    2.54        var multicore_list = List(default_multicore)
    2.55        var isabelle_identifier = default_isabelle_identifier
    2.56 +      var afp_partition = 0
    2.57        var more_settings: List[String] = Nil
    2.58        var fresh = false
    2.59        var init_settings: List[String] = Nil
    2.60 @@ -357,6 +368,7 @@
    2.61        default_heap * 2 + """ for x86_64)
    2.62      -M MULTICORE multicore configurations (see below)
    2.63      -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
    2.64 +    -P NUMBER    AFP partition number (0, 1, 2, default: 0=unrestricted)
    2.65      -U SIZE      maximal ML heap in MB (default: unbounded)
    2.66      -e TEXT      additional text for generated etc/settings
    2.67      -f           fresh build of Isabelle/Scala components (recommended)
    2.68 @@ -381,6 +393,7 @@
    2.69          "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
    2.70          "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse(_))),
    2.71          "N:" -> (arg => isabelle_identifier = arg),
    2.72 +        "P:" -> (arg => afp_partition = Value.Int.parse(arg)),
    2.73          "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
    2.74          "e:" -> (arg => more_settings = more_settings ::: List(arg)),
    2.75          "f" -> (_ => fresh = true),
    2.76 @@ -408,10 +421,10 @@
    2.77        val progress = new Console_Progress(stderr = true)
    2.78  
    2.79        val results =
    2.80 -        build_history(root, progress = progress, rev = rev, afp_rev = afp_rev,
    2.81 -          isabelle_identifier = isabelle_identifier, components_base = components_base,
    2.82 -          fresh = fresh, nonfree = nonfree, multicore_base = multicore_base,
    2.83 -          multicore_list = multicore_list, arch_64 = arch_64,
    2.84 +        build_history(Options.init(), root, progress = progress, rev = rev, afp_rev = afp_rev,
    2.85 +          afp_partition = afp_partition, isabelle_identifier = isabelle_identifier,
    2.86 +          components_base = components_base, fresh = fresh, nonfree = nonfree,
    2.87 +          multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
    2.88            heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
    2.89            max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
    2.90            verbose = verbose, build_tags = build_tags, build_args = build_args)
     3.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 14 15:44:21 2017 +0200
     3.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 14 16:59:45 2017 +0200
     3.3 @@ -58,7 +58,7 @@
     3.4              File.standard_path(isabelle_repos), isabelle_repos_test)
     3.5          for {
     3.6            (result, log_path) <-
     3.7 -            Build_History.build_history(isabelle_repos_test,
     3.8 +            Build_History.build_history(logger.options, isabelle_repos_test,
     3.9                rev = "build_history_base", fresh = true, build_args = List("HOL"))
    3.10          } {
    3.11            result.check