src/Pure/Admin/isabelle_cronjob.scala
changeset 67070 85e6c1ff5be3
parent 67049 0bb8369d10d6
child 67075 eada9bd5fff2
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Mon Nov 13 15:07:03 2017 +0100
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Nov 14 13:56:38 2017 +0100
     1.3 @@ -264,7 +264,7 @@
     1.4            detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))))
     1.5  
     1.6    private def remote_build_history(
     1.7 -    rev: String, afp_rev: Option[String], i: Int, user_home: Boolean, r: Remote_Build): Logger_Task =
     1.8 +    rev: String, afp_rev: Option[String], i: Int, r: Remote_Build): Logger_Task =
     1.9    {
    1.10      val task_name = "build_history-" + r.host
    1.11      Logger_Task(task_name, logger =>
    1.12 @@ -275,14 +275,6 @@
    1.13                val self_update = !r.shared_home
    1.14                val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
    1.15  
    1.16 -              if (user_home && r.shared_home) {
    1.17 -                ssh.execute("""
    1.18 -if [ ! -e /tmp/isabelle-isatest/contrib ]
    1.19 -then
    1.20 -  mkdir -p /tmp/isabelle-isatest && ln -s /home/isabelle/contrib /tmp/isabelle-isatest
    1.21 -fi""").check
    1.22 -              }
    1.23 -
    1.24                val results =
    1.25                  Build_History.remote_build_history(ssh,
    1.26                    isabelle_repos,
    1.27 @@ -293,7 +285,6 @@
    1.28                    rev = rev,
    1.29                    afp_rev = afp_rev,
    1.30                    options =
    1.31 -                    (if (user_home && r.shared_home) " -u /tmp/isabelle-isatest" else "") +
    1.32                      " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
    1.33                      " -f " + r.options,
    1.34                    args = "-o timeout=10800 " + r.args)
    1.35 @@ -448,9 +439,6 @@
    1.36      val hg = Mercurial.repository(isabelle_repos)
    1.37      val hg_graph = hg.graph()
    1.38  
    1.39 -    val user_home: String => Boolean =
    1.40 -      hg_graph.all_succs(List("19b6091c2137")).contains(_)
    1.41 -
    1.42      def history_base_filter(r: Remote_Build): Item => Boolean =
    1.43      {
    1.44        val base_rev = hg.id(r.history_base)
    1.45 @@ -475,7 +463,7 @@
    1.46                      for {
    1.47                        (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
    1.48                        (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r))
    1.49 -                    } yield remote_build_history(rev, afp_rev, i, user_home(rev), r)))),
    1.50 +                    } yield remote_build_history(rev, afp_rev, i, r)))),
    1.51                  Logger_Task("jenkins_logs", _ =>
    1.52                    Jenkins.download_logs(Jenkins.build_log_jobs, main_dir)),
    1.53                  Logger_Task("build_log_database",