src/Pure/Admin/build_history.scala
author wenzelm
Sun, 19 Mar 2017 13:05:06 +0100
changeset 65320 52861eebf58d
parent 65318 342efc382558
child 65588 b0d8d97198b3
permissions -rw-r--r--
access table via session_name: db may in principle contain multiple entries;
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"
64301
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
    99
  private val default_multicore = (1, 1)
64335
24e676390259 more ambitious default;
wenzelm
parents: 64305
diff changeset
   100
  private val default_heap = 1500
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,
64909
8007f10195af tuned signature;
wenzelm
parents: 64472
diff changeset
   105
    progress: Progress = No_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,
64301
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   112
    multicore_list: List[(Int, Int)] = List(default_multicore),
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,
64297
12a47f263122 support for free-form build tags;
wenzelm
parents: 64296
diff changeset
   118
    build_tags: List[String] = Nil,
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
   119
    build_args: List[String] = Nil): List[(Process_Result, Path)] =
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   120
  {
64031
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   121
    /* sanity checks */
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   122
64213
b265dd04d57d clarified file operations;
wenzelm
parents: 64194
diff changeset
   123
    if (File.eq(Path.explode("~~"), hg.root))
64046
5a6a7401c48b clarified sanity checks;
wenzelm
parents: 64044
diff changeset
   124
      error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
5a6a7401c48b clarified sanity checks;
wenzelm
parents: 64044
diff changeset
   125
64301
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   126
    for ((threads, _) <- multicore_list if threads < 1)
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   127
      error("Bad threads value < 1: " + threads)
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   128
    for ((_, processes) <- multicore_list if processes < 1)
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   129
      error("Bad processes value < 1: " + processes)
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   130
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   131
    if (heap < 100) error("Bad heap value < 100: " + heap)
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   132
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   133
    if (max_heap.isDefined && max_heap.get < heap)
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   134
      error("Bad max_heap value < heap: " + max_heap.get)
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   135
64031
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   136
    System.getenv("ISABELLE_SETTINGS_PRESENT") match {
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   137
      case null | "" =>
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   138
      case _ => error("Cannot run build_history within existing Isabelle settings environment")
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   139
    }
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   140
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   141
64049
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
   142
    /* init repository */
64031
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
   143
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   144
    hg.update(rev = rev, clean = true)
64049
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
   145
    progress.echo_if(verbose, hg.log(rev, options = "-l1"))
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   146
64232
367d83d6030e clarified hg.id operation, with explicit tip as default;
wenzelm
parents: 64231
diff changeset
   147
    val isabelle_version = hg.id(rev)
64049
ac3ed62c53c3 misc tuning and clarification;
wenzelm
parents: 64048
diff changeset
   148
    val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   149
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   150
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   151
    /* main */
64043
44b6c620c371 more thorought update of components;
wenzelm
parents: 64040
diff changeset
   152
64296
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64263
diff changeset
   153
    val build_host = Isabelle_System.hostname()
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   154
    val build_history_date = Date.now()
64296
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64263
diff changeset
   155
    val build_group_id = build_host + ":" + build_history_date.time.ms
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   156
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   157
    var first_build = true
64301
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   158
    for ((threads, processes) <- multicore_list) yield
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   159
    {
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   160
      /* init settings */
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   161
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
   162
      other_isabelle.init_settings(components_base, nonfree)
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   163
      other_isabelle.resolve_components(verbose)
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   164
      val ml_platform =
64188
f88bae1922c4 clarified modules;
wenzelm
parents: 64173
diff changeset
   165
        augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
64043
44b6c620c371 more thorought update of components;
wenzelm
parents: 64040
diff changeset
   166
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   167
      val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   168
      val isabelle_output_log = isabelle_output + Path.explode("log")
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   169
      val isabelle_base_log = isabelle_output + Path.explode("../base_log")
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   170
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   171
      if (first_build) {
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   172
        other_isabelle.resolve_components(verbose)
64376
68ace7f3d78f more thorough cleanup of lib/classes -- it may contain broken Pure.jar or copies of Scala libraries (in historic versions);
wenzelm
parents: 64353
diff changeset
   173
68ace7f3d78f more thorough cleanup of lib/classes -- it may contain broken Pure.jar or copies of Scala libraries (in historic versions);
wenzelm
parents: 64353
diff changeset
   174
        if (fresh)
68ace7f3d78f more thorough cleanup of lib/classes -- it may contain broken Pure.jar or copies of Scala libraries (in historic versions);
wenzelm
parents: 64353
diff changeset
   175
          Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   176
        other_isabelle.bash(
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   177
          "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
64376
68ace7f3d78f more thorough cleanup of lib/classes -- it may contain broken Pure.jar or copies of Scala libraries (in historic versions);
wenzelm
parents: 64353
diff changeset
   178
            "bin/isabelle jedit -b", redirect = true, echo = verbose).check
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   179
64213
b265dd04d57d clarified file operations;
wenzelm
parents: 64194
diff changeset
   180
        Isabelle_System.rm_tree(isabelle_base_log)
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   181
      }
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   182
64213
b265dd04d57d clarified file operations;
wenzelm
parents: 64194
diff changeset
   183
      Isabelle_System.rm_tree(isabelle_output)
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   184
      Isabelle_System.mkdirs(isabelle_output)
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   185
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   186
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   187
      /* build */
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   188
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   189
      if (multicore_base && !first_build && isabelle_base_log.is_dir)
64189
dfb63036c4f6 tuned signature;
wenzelm
parents: 64188
diff changeset
   190
        Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   191
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   192
      val build_start = Date.now()
64302
6de1aad1e70d report actual build_args;
wenzelm
parents: 64301
diff changeset
   193
      val build_args1 = List("-v", "-j" + processes) ::: build_args
64296
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64263
diff changeset
   194
      val build_result =
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64302
diff changeset
   195
        other_isabelle("build " + Bash.strings(build_args1), redirect = true, echo = verbose)
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   196
      val build_end = Date.now()
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   197
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   198
      val log_path =
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64189
diff changeset
   199
        other_isabelle.isabelle_home_user +
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64189
diff changeset
   200
          Build_Log.log_subdir(build_history_date) +
64297
12a47f263122 support for free-form build tags;
wenzelm
parents: 64296
diff changeset
   201
          Build_Log.log_filename(BUILD_HISTORY, build_history_date,
12a47f263122 support for free-form build tags;
wenzelm
parents: 64296
diff changeset
   202
            List(build_host, ml_platform, "M" + threads) ::: build_tags)
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   203
64296
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64263
diff changeset
   204
      val build_info =
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64263
diff changeset
   205
        Build_Log.Log_File(log_path.base.implode, build_result.out_lines).parse_build_info()
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64263
diff changeset
   206
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64263
diff changeset
   207
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64263
diff changeset
   208
      /* output log */
64120
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   209
65293
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   210
      val store = Sessions.store()
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   211
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   212
      val meta_info =
64300
3073688abbe9 clarified multiple props: result needs to fit on a single line within the log file;
wenzelm
parents: 64299
diff changeset
   213
        Build_Log.Prop.multiple(Build_Log.Prop.build_tags, build_tags) :::
64302
6de1aad1e70d report actual build_args;
wenzelm
parents: 64301
diff changeset
   214
        Build_Log.Prop.multiple(Build_Log.Prop.build_args, build_args1) :::
64296
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64263
diff changeset
   215
        List(
64298
wenzelm
parents: 64297
diff changeset
   216
          Build_Log.Prop.build_group_id -> build_group_id,
wenzelm
parents: 64297
diff changeset
   217
          Build_Log.Prop.build_id -> (build_host + ":" + build_start.time.ms),
wenzelm
parents: 64297
diff changeset
   218
          Build_Log.Prop.build_engine -> BUILD_HISTORY,
wenzelm
parents: 64297
diff changeset
   219
          Build_Log.Prop.build_host -> build_host,
wenzelm
parents: 64297
diff changeset
   220
          Build_Log.Prop.build_start -> Build_Log.print_date(build_start),
wenzelm
parents: 64297
diff changeset
   221
          Build_Log.Prop.build_end -> Build_Log.print_date(build_end),
wenzelm
parents: 64297
diff changeset
   222
          Build_Log.Prop.isabelle_version -> isabelle_version)
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   223
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   224
      val ml_statistics =
64120
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   225
        build_info.finished_sessions.flatMap(session_name =>
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   226
          {
65293
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   227
            val database = isabelle_output + store.database(session_name)
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   228
            val log_gz = isabelle_output + store.log_gz(session_name)
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   229
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   230
            val properties =
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   231
              if (database.is_file) {
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   232
                using(SQLite.open_database(database))(db =>
65320
52861eebf58d access table via session_name: db may in principle contain multiple entries;
wenzelm
parents: 65318
diff changeset
   233
                  store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
65293
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   234
              }
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   235
              else if (log_gz.is_file) {
65318
342efc382558 eliminated somewhat redundant inlined name (despite a7aa17a1f721);
wenzelm
parents: 65296
diff changeset
   236
                Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
65293
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   237
              }
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   238
              else Nil
a53a5ae88205 prefer database, but also accept log.gz from historic versions;
wenzelm
parents: 64909
diff changeset
   239
            properties.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
64120
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   240
          })
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   241
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   242
      val heap_sizes =
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   243
        build_info.finished_sessions.flatMap(session_name =>
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   244
          {
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   245
            val heap = isabelle_output + Path.explode(session_name)
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   246
            if (heap.is_file)
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   247
              Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   248
            else None
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   249
          })
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   250
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   251
      Isabelle_System.mkdirs(log_path.dir)
64253
a4718dfc9cd4 more compression for big log files;
wenzelm
parents: 64234
diff changeset
   252
      File.write_xz(log_path.ext("xz"),
64173
85ff21510ba9 tuned signature;
wenzelm
parents: 64162
diff changeset
   253
        terminate_lines(
64296
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64263
diff changeset
   254
          Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: build_result.out_lines :::
64120
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   255
          ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
64253
a4718dfc9cd4 more compression for big log files;
wenzelm
parents: 64234
diff changeset
   256
          heap_sizes), XZ.options(6))
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64052
diff changeset
   257
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   258
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   259
      /* next build */
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64118
diff changeset
   260
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   261
      if (multicore_base && first_build && isabelle_output_log.is_dir)
64189
dfb63036c4f6 tuned signature;
wenzelm
parents: 64188
diff changeset
   262
        Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log)
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   263
64260
5389ebfd576d more thorough cleanup;
wenzelm
parents: 64256
diff changeset
   264
      Isabelle_System.rm_tree(isabelle_output)
5389ebfd576d more thorough cleanup;
wenzelm
parents: 64256
diff changeset
   265
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   266
      first_build = false
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   267
64468
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64466
diff changeset
   268
      (build_result, log_path.ext("xz"))
64051
4dd9d9b28fd5 allow multiple threads configurations;
wenzelm
parents: 64050
diff changeset
   269
    }
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   270
  }
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   271
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   272
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   273
  /* command line entry point */
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   274
64301
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   275
  private object Multicore
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   276
  {
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   277
    private val Pat1 = """^(\d+)$""".r
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   278
    private val Pat2 = """^(\d+)x(\d+)$""".r
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   279
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   280
    def parse(s: String): (Int, Int) =
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   281
      s match {
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   282
        case Pat1(Value.Int(x)) => (x, 1)
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   283
        case Pat2(Value.Int(x), Value.Int(y)) => (x, y)
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   284
        case _ => error("Bad multicore configuration: " + quote(s))
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   285
      }
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   286
  }
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   287
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   288
  def main(args: Array[String])
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   289
  {
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   290
    Command_Line.tool0 {
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   291
      var multicore_base = false
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   292
      var components_base = ""
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   293
      var heap: Option[Int] = None
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   294
      var max_heap: Option[Int] = None
64301
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   295
      var multicore_list = List(default_multicore)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   296
      var isabelle_identifier = default_isabelle_identifier
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   297
      var more_settings: List[String] = Nil
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   298
      var fresh = false
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   299
      var arch_64 = false
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   300
      var nonfree = false
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   301
      var rev = default_rev
64297
12a47f263122 support for free-form build tags;
wenzelm
parents: 64296
diff changeset
   302
      var build_tags = List.empty[String]
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   303
      var verbose = false
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   304
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   305
      val getopts = Getopts("""
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   306
Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   307
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   308
  Options are:
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   309
    -B           first multicore build serves as base for scheduling information
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   310
    -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   311
    -H SIZE      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
64301
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   312
    -M MULTICORE multicore configurations (see below)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   313
    -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   314
    -U SIZE      maximal ML heap in MB (default: unbounded)
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   315
    -e TEXT      additional text for generated etc/settings
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   316
    -f           fresh build of Isabelle/Scala components (recommended)
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   317
    -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   318
    -n           include nonfree components
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   319
    -r REV       update to revision (default: """ + default_rev + """)
64297
12a47f263122 support for free-form build tags;
wenzelm
parents: 64296
diff changeset
   320
    -t TAG       free-form build tag (multiple occurrences possible)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   321
    -v           verbose
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   322
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   323
  Build Isabelle sessions from the history of another REPOSITORY clone,
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   324
  passing ARGS directly to its isabelle build tool.
64301
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   325
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   326
  Each MULTICORE configuration consists of one or two numbers (default 1):
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   327
  THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4.
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   328
""",
64052
72fa79eab7f6 added multicore_base option;
wenzelm
parents: 64051
diff changeset
   329
        "B" -> (_ => multicore_base = true),
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   330
        "C:" -> (arg => components_base = arg),
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   331
        "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
64301
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   332
        "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse(_))),
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   333
        "N:" -> (arg => isabelle_identifier = arg),
64036
a14fe26c0144 clarified heap options;
wenzelm
parents: 64034
diff changeset
   334
        "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   335
        "e:" -> (arg => more_settings = more_settings ::: List(arg)),
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   336
        "f" -> (_ => fresh = true),
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   337
        "m:" ->
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   338
          {
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   339
            case "32" | "x86" => arch_64 = false
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   340
            case "64" | "x86_64" => arch_64 = true
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   341
            case bad => error("Bad processor architecture: " + quote(bad))
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   342
          },
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   343
        "n" -> (_ => nonfree = true),
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   344
        "r:" -> (arg => rev = arg),
64297
12a47f263122 support for free-form build tags;
wenzelm
parents: 64296
diff changeset
   345
        "t:" -> (arg => build_tags = build_tags ::: List(arg)),
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   346
        "v" -> (_ => verbose = true))
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   347
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   348
      val more_args = getopts(args)
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   349
      val (root, build_args) =
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   350
        more_args match {
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   351
          case root :: build_args => (root, build_args)
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   352
          case _ => getopts.usage()
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   353
        }
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   354
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   355
      val hg = Mercurial.repository(Path.explode(root))
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   356
      val progress = new Console_Progress(stderr = true)
64346
5f49765a25ec process results immediately;
wenzelm
parents: 64335
diff changeset
   357
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   358
      val results =
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
   359
        build_history(hg, progress = progress, rev = rev, isabelle_identifier = isabelle_identifier,
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   360
          components_base = components_base, fresh = fresh, nonfree = nonfree,
64301
8053c882839f more flexible multicore configuration;
wenzelm
parents: 64300
diff changeset
   361
          multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   362
          heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   363
          max_heap = max_heap, more_settings = more_settings, verbose = verbose,
64297
12a47f263122 support for free-form build tags;
wenzelm
parents: 64296
diff changeset
   364
          build_tags = build_tags, build_args = build_args)
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   365
64472
c2191352e908 recovered Output.writeln for remote build_history (cf. ed8940d6295c), in order to have log files copied and removed;
wenzelm
parents: 64468
diff changeset
   366
      for ((_, log_path) <- results) Output.writeln(log_path.implode, stdout = true)
c2191352e908 recovered Output.writeln for remote build_history (cf. ed8940d6295c), in order to have log files copied and removed;
wenzelm
parents: 64468
diff changeset
   367
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
   368
      val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64160
diff changeset
   369
      if (rc != 0) sys.exit(rc)
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   370
    }
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   371
  }
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   372
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
64225
wenzelm
parents: 64223
diff changeset
   375
  /** remote build_history -- via command-line **/
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   376
64225
wenzelm
parents: 64223
diff changeset
   377
  def remote_build_history(
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64253
diff changeset
   378
    ssh: SSH.Session,
64227
wenzelm
parents: 64225
diff changeset
   379
    isabelle_repos_self: Path,
wenzelm
parents: 64225
diff changeset
   380
    isabelle_repos_other: Path,
wenzelm
parents: 64225
diff changeset
   381
    isabelle_repos_source: String = "http://isabelle.in.tum.de/repos/isabelle",
wenzelm
parents: 64225
diff changeset
   382
    self_update: Boolean = false,
64348
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64346
diff changeset
   383
    push_isabelle_home: Boolean = false,
64909
8007f10195af tuned signature;
wenzelm
parents: 64472
diff changeset
   384
    progress: Progress = No_Progress,
64227
wenzelm
parents: 64225
diff changeset
   385
    options: String = "",
64419
0f3b0a929c02 more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;
wenzelm
parents: 64376
diff changeset
   386
    args: String = ""): (List[(String, Bytes)], Process_Result) =
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   387
  {
64305
wenzelm
parents: 64304
diff changeset
   388
    val isabelle_admin = isabelle_repos_self + Path.explode("Admin")
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   389
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   390
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64253
diff changeset
   391
    /* prepare repository clones */
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   392
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64253
diff changeset
   393
    val isabelle_hg =
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64253
diff changeset
   394
      Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = Some(ssh))
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   395
64353
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   396
    val rev =
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   397
      if (self_update) {
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   398
        val rev =
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   399
          if (push_isabelle_home) {
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   400
            val isabelle_home_hg = Mercurial.repository(Path.explode("~~"))
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   401
            val rev = isabelle_home_hg.id()
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   402
            isabelle_home_hg.push(isabelle_hg.root_url, rev = rev, force = true)
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   403
            rev
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   404
          }
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   405
          else {
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   406
            isabelle_hg.pull()
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   407
            isabelle_hg.id()
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   408
          }
64348
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64346
diff changeset
   409
        isabelle_hg.update(rev = rev, clean = true)
64459
6f852a4c1b0e self_update of components, e.g. for vmnipkow9;
wenzelm
parents: 64453
diff changeset
   410
        ssh.execute(
6f852a4c1b0e self_update of components, e.g. for vmnipkow9;
wenzelm
parents: 64453
diff changeset
   411
          ssh.bash_path(isabelle_repos_self + Path.explode("bin/isabelle"))
6f852a4c1b0e self_update of components, e.g. for vmnipkow9;
wenzelm
parents: 64453
diff changeset
   412
            + " components -a").check
64353
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   413
        ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   414
        rev
64348
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64346
diff changeset
   415
      }
64353
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   416
      else "tip"
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   417
64348
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64346
diff changeset
   418
    val other_hg =
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64346
diff changeset
   419
      Mercurial.setup_repository(
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64346
diff changeset
   420
        ssh.bash_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh))
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64346
diff changeset
   421
    other_hg.pull(isabelle_hg.root.implode)
64353
8f628de5108b more explicit rev (tip);
wenzelm
parents: 64348
diff changeset
   422
    other_hg.update(rev = rev, clean = true)
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   423
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   424
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64253
diff changeset
   425
    /* Admin/build_history */
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   426
64419
0f3b0a929c02 more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;
wenzelm
parents: 64376
diff changeset
   427
    val process_result =
0f3b0a929c02 more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;
wenzelm
parents: 64376
diff changeset
   428
      ssh.execute(
0f3b0a929c02 more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;
wenzelm
parents: 64376
diff changeset
   429
        ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
0f3b0a929c02 more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;
wenzelm
parents: 64376
diff changeset
   430
          ssh.bash_path(isabelle_repos_other) + " " + args,
64468
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64466
diff changeset
   431
        progress_stdout = progress.echo(_),
64453
075c077a6e29 ignore interrupts from underlying process, e.g. due to out-of-memory situation in ML_Process (see also build.scala);
wenzelm
parents: 64419
diff changeset
   432
        progress_stderr = progress.echo(_),
075c077a6e29 ignore interrupts from underlying process, e.g. due to out-of-memory situation in ML_Process (see also build.scala);
wenzelm
parents: 64419
diff changeset
   433
        strict = false)
64346
5f49765a25ec process results immediately;
wenzelm
parents: 64335
diff changeset
   434
64468
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64466
diff changeset
   435
    val result =
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64466
diff changeset
   436
      for (line <- process_result.out_lines)
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64466
diff changeset
   437
      yield {
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64466
diff changeset
   438
        val log = Path.explode(line)
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64466
diff changeset
   439
        val bytes = ssh.read_bytes(log)
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64466
diff changeset
   440
        ssh.rm(log)
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64466
diff changeset
   441
        (log.base.implode, bytes)
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64466
diff changeset
   442
      }
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64466
diff changeset
   443
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64466
diff changeset
   444
    (result, process_result)
64223
9d5b9f41df77 remove invocation of build_history: results are reported via stdout;
wenzelm
parents: 64213
diff changeset
   445
  }
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   446
}