src/Pure/Admin/build_history.scala
author wenzelm
Sat, 15 Oct 2016 21:08:04 +0200
changeset 64232 367d83d6030e
parent 64231 dbc8294c75d3
child 64233 ef6f7e8a018c
permissions -rw-r--r--
clarified hg.id operation, with explicit tip as default;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64160
1eea419fab65 clarified files;
wenzelm
parents: 64155
diff changeset
     1
/*  Title:      Pure/Admin/build_history.scala
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     3
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     4
Build other history versions.
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     5
*/
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     6
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     7
package isabelle
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     8
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     9
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    10
import java.io.{File => JFile}
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
    11
import java.time.format.DateTimeFormatter
64118
0996fab2ec03 modernized;
wenzelm
parents: 64117
diff changeset
    12
import java.util.Locale
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    13
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    14
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    15
object Build_History
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    16
{
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
    17
  /* log files */
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
    18
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
    19
  val BUILD_HISTORY = "build_history"
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
    20
  val META_INFO_MARKER = "\fmeta_info = "
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
    21
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
    22
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    23
  /* augment settings */
64050
wenzelm
parents: 64049
diff changeset
    24
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    25
  def augment_settings(
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    26
    other_isabelle: Other_Isabelle,
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    27
    threads: Int,
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    28
    arch_64: Boolean = false,
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    29
    heap: Int = default_heap,
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    30
    max_heap: Option[Int] = None,
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    31
    more_settings: List[String]): String =
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    32
  {
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    33
    val (ml_platform, ml_settings) =
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    34
    {
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    35
      val windows_32 = "x86-windows"
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    36
      val windows_64 = "x86_64-windows"
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    37
      val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    38
      val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    39
      val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
64049
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
    40
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    41
      val polyml_home =
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    42
        try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    43
        catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
64049
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
    44
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    45
      def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
64049
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
    46
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    47
      def err(platform: String): Nothing =
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    48
        error("Platform " + platform + " unavailable on this machine")
64050
wenzelm
parents: 64049
diff changeset
    49
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    50
      def check_dir(platform: String): Boolean =
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    51
        platform != "" && ml_home(platform).is_dir
64050
wenzelm
parents: 64049
diff changeset
    52
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    53
      val ml_platform =
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    54
        if (Platform.is_windows && arch_64) {
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    55
          if (check_dir(windows_64)) windows_64 else err(windows_64)
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    56
        }
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    57
        else if (Platform.is_windows && !arch_64) {
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    58
          if (check_dir(windows_32)) windows_32
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    59
          else platform_32  // x86-cygwin
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    60
        }
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    61
        else {
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    62
          val (platform, platform_name) =
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    63
            if (arch_64) (platform_64, "x86_64-" + platform_family)
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    64
            else (platform_32, "x86-" + platform_family)
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    65
          if (check_dir(platform)) platform else err(platform_name)
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    66
        }
64050
wenzelm
parents: 64049
diff changeset
    67
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    68
      val ml_options =
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    69
        "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    70
        " --gcthreads " + threads +
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    71
        (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
64050
wenzelm
parents: 64049
diff changeset
    72
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    73
      (ml_platform,
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    74
        List(
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    75
          "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    76
          "ML_PLATFORM=" + quote(ml_platform),
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    77
          "ML_OPTIONS=" + quote(ml_options)))
64050
wenzelm
parents: 64049
diff changeset
    78
    }
wenzelm
parents: 64049
diff changeset
    79
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    80
    val thread_settings =
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    81
      List(
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    82
        "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    83
        "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
64050
wenzelm
parents: 64049
diff changeset
    84
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    85
    val settings =
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    86
      List(ml_settings, thread_settings) :::
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    87
        (if (more_settings.isEmpty) Nil else List(more_settings))
64050
wenzelm
parents: 64049
diff changeset
    88
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    89
    File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
64050
wenzelm
parents: 64049
diff changeset
    90
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
    91
    ml_platform
64049
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
    92
  }
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
    93
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
    94
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
    95
64050
wenzelm
parents: 64049
diff changeset
    96
  /** build_history **/
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    97
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    98
  private val default_rev = "tip"
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    99
  private val default_threads = 1
64034
51bf28aa18a5 more ambitious default as in former isatest;
wenzelm
parents: 64032
diff changeset
   100
  private val default_heap = 1000
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   101
  private val default_isabelle_identifier = "build_history"
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   102
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   103
  def build_history(
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   104
    hg: Mercurial.Repository,
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
   105
    progress: Progress = Ignore_Progress,
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   106
    rev: String = default_rev,
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   107
    isabelle_identifier: String = default_isabelle_identifier,
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   108
    components_base: String = "",
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   109
    fresh: Boolean = false,
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   110
    nonfree: Boolean = false,
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   111
    multicore_base: Boolean = false,
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   112
    threads_list: List[Int] = List(default_threads),
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   113
    arch_64: Boolean = false,
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   114
    heap: Int = default_heap,
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   115
    max_heap: Option[Int] = None,
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   116
    more_settings: List[String] = Nil,
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   117
    verbose: Boolean = false,
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
   118
    build_args: List[String] = Nil): List[(Process_Result, Path)] =
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   119
  {
64031
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   120
    /* sanity checks */
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   121
64213
b265dd04d57d clarified file operations;
wenzelm
parents: 64194
diff changeset
   122
    if (File.eq(Path.explode("~~"), hg.root))
64046
5a6a7401c48b clarified sanity checks;
wenzelm
parents: 64044
diff changeset
   123
      error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
5a6a7401c48b clarified sanity checks;
wenzelm
parents: 64044
diff changeset
   124
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   125
    for (threads <- threads_list if threads < 1) error("Bad threads value < 1: " + threads)
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   126
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   127
    if (heap < 100) error("Bad heap value < 100: " + heap)
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   128
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   129
    if (max_heap.isDefined && max_heap.get < heap)
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   130
      error("Bad max_heap value < heap: " + max_heap.get)
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   131
64031
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   132
    System.getenv("ISABELLE_SETTINGS_PRESENT") match {
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   133
      case null | "" =>
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   134
      case _ => error("Cannot run build_history within existing Isabelle settings environment")
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   135
    }
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   136
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   137
64049
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
   138
    /* init repository */
64031
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   139
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   140
    hg.update(rev = rev, clean = true)
64049
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
   141
    progress.echo_if(verbose, hg.log(rev, options = "-l1"))
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   142
64232
367d83d6030e clarified hg.id operation, with explicit tip as default;
wenzelm
parents: 64231
diff changeset
   143
    val isabelle_version = hg.id(rev)
64049
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
   144
    val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   145
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   146
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   147
    /* main */
64043
44b6c620c371 more thorought update of components;
wenzelm
parents: 64040
diff changeset
   148
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   149
    val build_history_date = Date.now()
64139
387c811cad6a tuned signature;
wenzelm
parents: 64138
diff changeset
   150
    val build_host = Isabelle_System.hostname()
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   151
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   152
    var first_build = true
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   153
    for (threads <- threads_list) yield
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   154
    {
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   155
      /* init settings */
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   156
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
   157
      other_isabelle.init_settings(components_base, nonfree)
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   158
      other_isabelle.resolve_components(verbose)
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   159
      val ml_platform =
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
   160
        augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
64043
44b6c620c371 more thorought update of components;
wenzelm
parents: 64040
diff changeset
   161
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   162
      val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   163
      val isabelle_output_log = isabelle_output + Path.explode("log")
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   164
      val isabelle_base_log = isabelle_output + Path.explode("../base_log")
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   165
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   166
      if (first_build) {
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   167
        other_isabelle.resolve_components(verbose)
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   168
        other_isabelle.bash(
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   169
          "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   170
            "bin/isabelle jedit -b" + (if (fresh) " -f" else ""),
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   171
          redirect = true, echo = verbose).check
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   172
64213
b265dd04d57d clarified file operations;
wenzelm
parents: 64194
diff changeset
   173
        Isabelle_System.rm_tree(isabelle_base_log)
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   174
      }
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   175
64213
b265dd04d57d clarified file operations;
wenzelm
parents: 64194
diff changeset
   176
      Isabelle_System.rm_tree(isabelle_output)
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   177
      Isabelle_System.mkdirs(isabelle_output)
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   178
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   179
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   180
      /* build */
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   181
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   182
      if (multicore_base && !first_build && isabelle_base_log.is_dir)
64189
dfb63036c4f6 tuned signature;
wenzelm
parents: 64188
diff changeset
   183
        Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   184
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   185
      val build_start = Date.now()
64121
f2c8f6b11dcf enforce detailed build log;
wenzelm
parents: 64120
diff changeset
   186
      val res =
f2c8f6b11dcf enforce detailed build log;
wenzelm
parents: 64120
diff changeset
   187
        other_isabelle("build -v " + File.bash_args(build_args), redirect = true, echo = verbose)
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   188
      val build_end = Date.now()
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   189
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   190
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   191
      /* output log */
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   192
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   193
      val log_path =
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64189
diff changeset
   194
        other_isabelle.isabelle_home_user +
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64189
diff changeset
   195
          Build_Log.log_subdir(build_history_date) +
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64189
diff changeset
   196
          Build_Log.log_filename(
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64189
diff changeset
   197
            BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   198
64120
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   199
      val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   200
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   201
      val meta_info =
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   202
        List(Build_Log.Field.build_engine -> BUILD_HISTORY,
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   203
          Build_Log.Field.build_host -> build_host,
64155
646c4d6a6a02 tuned signature;
wenzelm
parents: 64151
diff changeset
   204
          Build_Log.Field.build_start -> Build_Log.print_date(build_start),
646c4d6a6a02 tuned signature;
wenzelm
parents: 64151
diff changeset
   205
          Build_Log.Field.build_end -> Build_Log.print_date(build_end),
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   206
          Build_Log.Field.isabelle_version -> isabelle_version)
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   207
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   208
      val ml_statistics =
64120
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   209
        build_info.finished_sessions.flatMap(session_name =>
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   210
          {
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   211
            val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   212
            if (session_log.is_file) {
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   213
              Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   214
                ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   215
            }
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   216
            else Nil
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   217
          })
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   218
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   219
      val heap_sizes =
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   220
        build_info.finished_sessions.flatMap(session_name =>
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   221
          {
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   222
            val heap = isabelle_output + Path.explode(session_name)
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   223
            if (heap.is_file)
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   224
              Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   225
            else None
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   226
          })
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   227
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   228
      Isabelle_System.mkdirs(log_path.dir)
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   229
      File.write_gzip(log_path,
64173
85ff21510ba9 tuned signature;
wenzelm
parents: 64162
diff changeset
   230
        terminate_lines(
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   231
          Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
64120
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   232
          ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   233
          heap_sizes))
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   234
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   235
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   236
      /* next build */
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   237
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   238
      if (multicore_base && first_build && isabelle_output_log.is_dir)
64189
dfb63036c4f6 tuned signature;
wenzelm
parents: 64188
diff changeset
   239
        Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log)
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   240
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   241
      first_build = false
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   242
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
   243
      (res, log_path)
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   244
    }
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   245
  }
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   246
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   247
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   248
  /* command line entry point */
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   249
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   250
  def main(args: Array[String])
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   251
  {
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   252
    Command_Line.tool0 {
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   253
      var multicore_base = false
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   254
      var components_base = ""
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   255
      var heap: Option[Int] = None
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   256
      var max_heap: Option[Int] = None
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   257
      var threads_list = List(default_threads)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   258
      var isabelle_identifier = default_isabelle_identifier
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   259
      var more_settings: List[String] = Nil
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   260
      var fresh = false
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   261
      var arch_64 = false
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   262
      var nonfree = false
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   263
      var rev = default_rev
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   264
      var verbose = false
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   265
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   266
      val getopts = Getopts("""
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   267
Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   268
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   269
  Options are:
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   270
    -B           first multicore build serves as base for scheduling information
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   271
    -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   272
    -H SIZE      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   273
    -M THREADS   multicore configurations (comma-separated list, default: """ + default_threads + """)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   274
    -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   275
    -U SIZE      maximal ML heap in MB (default: unbounded)
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   276
    -e TEXT      additional text for generated etc/settings
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   277
    -f           fresh build of Isabelle/Scala components (recommended)
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   278
    -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   279
    -n           include nonfree components
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   280
    -r REV       update to revision (default: """ + default_rev + """)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   281
    -v           verbose
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   282
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   283
  Build Isabelle sessions from the history of another REPOSITORY clone,
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   284
  passing ARGS directly to its isabelle build tool.
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   285
""",
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   286
        "B" -> (_ => multicore_base = true),
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   287
        "C:" -> (arg => components_base = arg),
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   288
        "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   289
        "M:" -> (arg => threads_list = space_explode(',', arg).map(Value.Int.parse(_))),
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   290
        "N:" -> (arg => isabelle_identifier = arg),
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   291
        "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   292
        "e:" -> (arg => more_settings = more_settings ::: List(arg)),
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   293
        "f" -> (_ => fresh = true),
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   294
        "m:" ->
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   295
          {
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   296
            case "32" | "x86" => arch_64 = false
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   297
            case "64" | "x86_64" => arch_64 = true
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   298
            case bad => error("Bad processor architecture: " + quote(bad))
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   299
          },
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   300
        "n" -> (_ => nonfree = true),
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   301
        "r:" -> (arg => rev = arg),
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   302
        "v" -> (_ => verbose = true))
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   303
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   304
      val more_args = getopts(args)
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   305
      val (root, build_args) =
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   306
        more_args match {
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   307
          case root :: build_args => (root, build_args)
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   308
          case _ => getopts.usage()
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   309
        }
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   310
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   311
      val hg = Mercurial.repository(Path.explode(root))
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   312
      val progress = new Console_Progress(stderr = true)
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   313
      val results =
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
   314
        build_history(hg, progress = progress, rev = rev, isabelle_identifier = isabelle_identifier,
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   315
          components_base = components_base, fresh = fresh, nonfree = nonfree,
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   316
          multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64,
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   317
          heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   318
          max_heap = max_heap, more_settings = more_settings, verbose = verbose,
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   319
          build_args = build_args)
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   320
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
   321
      for ((_, log_path) <- results)
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
   322
        Output.writeln(log_path.implode, stdout = true)
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
   323
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
   324
      val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   325
      if (rc != 0) sys.exit(rc)
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   326
    }
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   327
  }
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   328
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   329
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   330
64225
wenzelm
parents: 64223
diff changeset
   331
  /** remote build_history -- via command-line **/
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   332
64225
wenzelm
parents: 64223
diff changeset
   333
  def remote_build_history(
64227
wenzelm
parents: 64225
diff changeset
   334
    session: SSH.Session,
wenzelm
parents: 64225
diff changeset
   335
    isabelle_repos_self: Path,
wenzelm
parents: 64225
diff changeset
   336
    isabelle_repos_other: Path,
wenzelm
parents: 64225
diff changeset
   337
    isabelle_repos_source: String = "http://isabelle.in.tum.de/repos/isabelle",
wenzelm
parents: 64225
diff changeset
   338
    self_update: Boolean = false,
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   339
    progress: Progress = Ignore_Progress,
64227
wenzelm
parents: 64225
diff changeset
   340
    options: String = "",
wenzelm
parents: 64225
diff changeset
   341
    args: String = ""): List[(String, Bytes)] =
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   342
  {
64227
wenzelm
parents: 64225
diff changeset
   343
    using(session.sftp())(sftp =>
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   344
      {
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64227
diff changeset
   345
        val isabelle_admin = sftp.path(isabelle_repos_self + Path.explode("Admin"))
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   346
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   347
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   348
        /* prepare repository clones */
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   349
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   350
        val isabelle_hg =
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64227
diff changeset
   351
          Mercurial.setup_repository(
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64227
diff changeset
   352
            isabelle_repos_source, isabelle_repos_self, ssh = Some(session))
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   353
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   354
        if (self_update) {
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   355
          isabelle_hg.pull()
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   356
          isabelle_hg.update(clean = true)
64227
wenzelm
parents: 64225
diff changeset
   357
          session.execute(File.bash_string(isabelle_admin + "/build") + " jars_fresh").check
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   358
        }
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   359
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64227
diff changeset
   360
        Mercurial.setup_repository(
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64227
diff changeset
   361
          sftp.path(isabelle_repos_self), isabelle_repos_other, ssh = Some(session))
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   362
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   363
64225
wenzelm
parents: 64223
diff changeset
   364
        /* Admin/build_history */
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   365
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   366
        val result =
64227
wenzelm
parents: 64225
diff changeset
   367
          session.execute(
64225
wenzelm
parents: 64223
diff changeset
   368
            File.bash_string(isabelle_admin + "/build_history") + " " + options + " " +
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64227
diff changeset
   369
              File.bash_string(sftp.path(isabelle_repos_other)) + " " + args,
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   370
            progress_stderr = progress.echo(_))
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   371
64227
wenzelm
parents: 64225
diff changeset
   372
        result.check.out_lines.map(log => (Path.explode(log).base.implode, sftp.read_bytes(log)))
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   373
      })
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   374
  }
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   375
}