# HG changeset patch # User wenzelm # Date 1520354492 -3600 # Node ID 5437491732d2244fe3ec3439a4e8905f67b0cb05 # Parent 4a7ed678785c0e879616464c8bd608c218e95c8d build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory; diff -r 4a7ed678785c -r 5437491732d2 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Tue Mar 06 16:54:13 2018 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Tue Mar 06 17:41:32 2018 +0100 @@ -23,7 +23,6 @@ val isabelle_repos_source = "https://isabelle.in.tum.de/repos/isabelle" val isabelle_repos = main_dir + Path.explode("isabelle") - val isabelle_repos_test = main_dir + Path.explode("isabelle-test") val afp_repos = main_dir + Path.explode("AFP") val build_log_dirs = @@ -81,17 +80,22 @@ val build_history_base = Logger_Task("build_history_base", logger => { - val hg = - Mercurial.setup_repository( - File.standard_path(isabelle_repos), isabelle_repos_test) - for { - (result, log_path) <- - Build_History.build_history(logger.options, isabelle_repos_test, - rev = "build_history_base", fresh = true, build_args = List("HOL")) - } { - result.check - File.move(log_path, logger.log_dir + log_path.base) - } + using(logger.ssh_context.open_session("lxbroy10"))(ssh => + { + val results = + Build_History.remote_build_history(ssh, + isabelle_repos, + isabelle_repos.ext("build_history_base"), + isabelle_identifier = "cronjob_build_history", + self_update = true, + rev = "build_history_base", + options = "-f", + args = "HOL") + + for ((log_name, bytes) <- results) { + Bytes.write(logger.log_dir + Path.explode(log_name), bytes) + } + }) }) @@ -146,7 +150,7 @@ proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, - remote_home: Boolean = true, // false for lxbroy/homebroy + remote_home: Boolean = false, historic: Boolean = false, history: Int = 0, history_base: String = "build_history_base", @@ -508,8 +512,9 @@ run_now( SEQ(List( init, + build_history_base, PAR( - SEQ(List(build_release, build_history_base)) :: + build_release :: List(remote_builds1, remote_builds2).map(remote_builds => SEQ(List( PAR(remote_builds.map(_.filter(_.active)).map(seq =>