# HG changeset patch # User wenzelm # Date 1508682924 -7200 # Node ID a9d5b59c3e122a0ab0629b91a26e317e04d35bdd # Parent c08d7349774eaae0a9b70066b4cb5dedda8969e6# Parent a02b5bb3fad7a16ce96ea0e78c96012bcfb6c823 merged diff -r c08d7349774e -r a9d5b59c3e12 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Sun Oct 22 11:59:44 2017 +0200 +++ b/Admin/components/components.sha1 Sun Oct 22 16:35:24 2017 +0200 @@ -156,6 +156,7 @@ 5fbcab1da2b5eb97f24da2590ece189d55b3a105 polyml-5.7.tar.gz 853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz c629cd499a724bbe37b962f727e4ff340c50299d polyml-test-8529546198aa.tar.gz +2b7c02b67feb2f44dda6938a7244f4257e7c580c polyml-test-905dae2ebfda.tar.gz b4ceeaac47f3baae41c2491a8368b03217946166 polyml-test-e7a662f8f9c4.tar.gz 53123dc011b2d4b4e8fe307f3c9fa355718ad01a postgresql-42.1.1.tar.gz 3a5d31377ec07a5069957f5477a4848cfc89a594 postgresql-42.1.4.tar.gz @@ -218,4 +219,5 @@ 86e721296c400ada440e4a9ce11b9e845eec9e25 z3-4.3.0.tar.gz a8917c31b31c182edeec0aaa48870844960c8a61 z3-4.3.2pre-1.tar.gz 06b30757ff23aefbc30479785c212685ffd39f4d z3-4.3.2pre.tar.gz +93e7e4bddc6afcf87fe2b6656cfcb1b1acd0a4f8 z3-4.4.0pre-1.tar.gz 517ba7b94c1985416c5b411c8ae84456367eb231 z3-4.4.0pre.tar.gz diff -r c08d7349774e -r a9d5b59c3e12 Admin/polyml/settings --- a/Admin/polyml/settings Sun Oct 22 11:59:44 2017 +0200 +++ b/Admin/polyml/settings Sun Oct 22 16:35:24 2017 +0200 @@ -48,15 +48,19 @@ case "$ML_PLATFORM" in x86_64-windows) + POLYML_EXE="$ML_HOME/poly.exe" ML_OPTIONS="-H 1000 --codepage utf8" ;; x86-windows) + POLYML_EXE="$ML_HOME/poly.exe" ML_OPTIONS="-H 500 --codepage utf8" ;; x86_64-*) + POLYML_EXE="$ML_HOME/poly" ML_OPTIONS="-H 1000" ;; *) + POLYML_EXE="$ML_HOME/poly" ML_OPTIONS="-H 500" ;; esac diff -r c08d7349774e -r a9d5b59c3e12 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Sun Oct 22 11:59:44 2017 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Oct 22 16:35:24 2017 +0200 @@ -13,7 +13,7 @@ object Isabelle_Cronjob { - /* file-system state: owned by main cronjob */ + /* global resources: owned by main cronjob */ val main_dir = Path.explode("~/cronjob") val main_state_file = main_dir + Path.explode("run/main.state") @@ -26,6 +26,9 @@ val jenkins_jobs = "identify" :: Jenkins.build_log_jobs + val build_log_dirs = + List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log")) + /** particular tasks **/ @@ -130,13 +133,6 @@ def profile: Build_Status.Profile = Build_Status.Profile(description, history = history, afp = afp, sql = sql) - def history_base_filter(hg: Mercurial.Repository): Item => Boolean = - { - val rev0 = hg.id(history_base) - val nodes = hg.graph().all_succs(List(rev0)).toSet - (item: Item) => nodes(item.isabelle_version) - } - def pick( options: Options, rev: String = "", @@ -192,7 +188,7 @@ detect = Build_Log.Prop.build_start + " < date '2017-03-03'")) - val remote_builds: List[List[Remote_Build]] = + val remote_builds1: List[List[Remote_Build]] = { List( List(Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8", @@ -241,12 +237,6 @@ " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", args = "-a", detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))), - List( - Remote_Build("AFP slow", "lrzcloud1", shared_home = false, - options = "-m64 -M6 -U30000 -s10 -t AFP", - args = "-g slow", - afp = true, - detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))) ) ::: { for { (host, n) <- List("lxbroy6" -> 1, "lxbroy7" -> 2) } @@ -260,6 +250,15 @@ } } + val remote_builds2: List[List[Remote_Build]] = + List( + List( + Remote_Build("AFP slow", "lrzcloud1", shared_home = false, + options = "-m64 -M6 -U30000 -s10 -t AFP", + args = "-g slow", + afp = true, + detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")))) + private def remote_build_history( rev: String, afp_rev: Option[String], i: Int, r: Remote_Build): Logger_Task = { @@ -295,7 +294,7 @@ } val build_status_profiles: List[Build_Status.Profile] = - (remote_builds_old :: remote_builds).flatten.map(_.profile) + (remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile) @@ -431,29 +430,42 @@ }) + /* repository structure */ + + val hg = Mercurial.repository(isabelle_repos) + val hg_graph = hg.graph() + val rev = hg.id() + + def history_base_filter(r: Remote_Build): Item => Boolean = + { + val base_rev = hg.id(r.history_base) + val nodes = hg_graph.all_succs(List(base_rev)).toSet + (item: Item) => nodes(item.isabelle_version) + } + + /* main */ val main_start_date = Date.now() File.write(main_state_file, main_start_date + " " + log_service.hostname) - val hg = Mercurial.repository(isabelle_repos) - val rev = hg.id() - run(main_start_date, Logger_Task("isabelle_cronjob", logger => run_now( SEQ(List(build_release, build_history_base, - PAR(remote_builds.map(seq => - SEQ( - for { - (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex) - (isabelle_rev, afp_rev) <- r.pick(logger.options, rev, r.history_base_filter(hg)) - } yield remote_build_history(isabelle_rev, afp_rev, i, r)))), - Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)), - Logger_Task("build_log_database", - logger => Isabelle_Devel.build_log_database(logger.options)), - Logger_Task("build_status", - logger => Isabelle_Devel.build_status(logger.options))))))) + PAR(List(remote_builds1, remote_builds2).map(remote_builds => + SEQ(List( + PAR(remote_builds.map(seq => + SEQ( + for { + (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex) + (isabelle_rev, afp_rev) <- r.pick(logger.options, rev, history_base_filter(r)) + } yield remote_build_history(isabelle_rev, afp_rev, i, r)))), + Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)), + Logger_Task("build_log_database", + logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)), + Logger_Task("build_status", + logger => Isabelle_Devel.build_status(logger.options))))))))))) log_service.shutdown() diff -r c08d7349774e -r a9d5b59c3e12 src/Pure/Admin/isabelle_devel.scala --- a/src/Pure/Admin/isabelle_devel.scala Sun Oct 22 11:59:44 2017 +0200 +++ b/src/Pure/Admin/isabelle_devel.scala Sun Oct 22 16:35:24 2017 +0200 @@ -15,9 +15,6 @@ val BUILD_LOG_DB = "build_log.db" val BUILD_STATUS = "build_status" - val standard_log_dirs = - List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log")) - /* index */ @@ -67,7 +64,7 @@ /* maintain build_log database */ - def build_log_database(options: Options, log_dirs: List[Path] = standard_log_dirs) + def build_log_database(options: Options, log_dirs: List[Path]) { val store = Build_Log.store(options) using(store.open_database())(db => diff -r c08d7349774e -r a9d5b59c3e12 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Sun Oct 22 11:59:44 2017 +0200 +++ b/src/Pure/General/mercurial.scala Sun Oct 22 16:35:24 2017 +0200 @@ -16,6 +16,9 @@ object Mercurial { + type Graph = isabelle.Graph[String, Unit] + + /* command-line syntax */ def optional(s: String, prefix: String = ""): String = @@ -119,7 +122,7 @@ def known_files(): List[String] = hg.command("status", options = "--modified --added --clean --no-status").check.out_lines - def graph(): Graph[String, Unit] = + def graph(): Graph = { val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r val log_result =