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;
authorwenzelm
Tue, 06 Mar 2018 17:41:32 +0100
changeset 67774 5437491732d2
parent 67773 4a7ed678785c
child 67775 8fe8424ff0d3
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;
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 =>