src/Pure/Tools/build_history.scala
author wenzelm
Tue, 04 Oct 2016 14:20:26 +0200
changeset 64032 46c1ffc78d73
parent 64031 eef8a3f8ef4a
child 64034 51bf28aa18a5
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/build_history.scala
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}
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    11
import java.util.Calendar
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    12
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
object Build_History
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    15
{
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    16
  /* build_history */
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    17
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    18
  private val default_rev = "tip"
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    19
  private val default_threads = 1
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    20
  private val default_heap = 500
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    21
  private val default_isabelle_identifier = "build_history"
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    22
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    23
  def build_history(
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    24
    hg: Mercurial.Repository,
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    25
    rev: String = default_rev,
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    26
    isabelle_identifier: String = default_isabelle_identifier,
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    27
    components_base: String = "",
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
    28
    fresh: Boolean = false,
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    29
    nonfree: Boolean = false,
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    30
    threads: Int = default_threads,
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    31
    arch_64: Boolean = false,
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    32
    heap: Int = default_heap,
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    33
    more_settings: List[String] = Nil,
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
    34
    verbose: Boolean = false,
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
    35
    build_args: List[String] = Nil): Process_Result =
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    36
  {
64031
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    37
    /* sanity checks */
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    38
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    39
    if (threads < 1) error("Bad threads value < 1: " + threads)
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    40
    if (heap < 100) error("Bad heap value < 100: " + heap)
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    41
64031
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    42
    System.getenv("ISABELLE_SETTINGS_PRESENT") match {
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    43
      case null | "" =>
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    44
      case _ => error("Cannot run build_history within existing Isabelle settings environment")
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    45
    }
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    46
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    47
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    48
    /* purge repository */
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    49
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    50
    hg.update(rev = rev, clean = true)
64027
4a33d740c9dc proper log output;
wenzelm
parents: 64026
diff changeset
    51
    if (verbose) Output.writeln(hg.log(rev, options = "-l1"))
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    52
64031
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    53
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    54
    /* invoke isabelle tools */
eef8a3f8ef4a more sanity checks;
wenzelm
parents: 64030
diff changeset
    55
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    56
    def bash(script: String): Process_Result =
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    57
      Isabelle_System.bash("env ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) +
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    58
        " " + script, cwd = hg.root.file, env = null)
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    59
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    60
    def isabelle(cmdline: String): Process_Result = bash("bin/isabelle " + cmdline)
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    61
    val isabelle_home_user: Path = Path.explode(isabelle("getenv -b ISABELLE_HOME_USER").check.out)
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    62
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    63
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    64
    /* reset settings */
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    65
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    66
    val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    67
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    68
    if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    69
      error("Cannot proceed with existing user settings file: " + etc_settings)
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    70
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    71
    Isabelle_System.mkdirs(etc_settings.dir)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    72
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    73
    File.write(etc_settings,
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    74
      "# generated by Isabelle " + Calendar.getInstance.getTime + "\n" +
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    75
      "#-*- shell-script -*- :mode=shellscript:\n")
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    76
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    77
64032
wenzelm
parents: 64031
diff changeset
    78
    /* initial settings */
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    79
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    80
    val component_settings =
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    81
    {
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    82
      val components_base_path =
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    83
        if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    84
        else Path.explode(components_base).expand
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    85
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    86
      val catalogs =
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    87
        if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    88
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    89
      catalogs.map(catalog =>
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    90
        "init_components " + File.bash_path(components_base_path) +
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    91
          " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    92
    }
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    93
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    94
    File.append(etc_settings, "\n" + Library.terminate_lines(component_settings))
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    95
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    96
64032
wenzelm
parents: 64031
diff changeset
    97
    /* augmented settings */
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    98
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
    99
    val ml_settings =
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   100
    {
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   101
      val windows_32 = "x86-windows"
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   102
      val windows_64 = "x86_64-windows"
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   103
      val platform_32 = isabelle("getenv -b ISABELLE_PLATFORM32").check.out
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   104
      val platform_64 = isabelle("getenv -b ISABELLE_PLATFORM64").check.out
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   105
      val platform_family = isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   106
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   107
      val polyml_home = Path.explode(isabelle("getenv -b ML_HOME").check.out).dir
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   108
      def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   109
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   110
      def err(platform: String): Nothing =
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   111
        error("Platform " + platform + " unavailable on this machine")
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   112
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   113
      def check_dir(platform: String): Boolean =
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   114
        platform != "" && ml_home(platform).is_dir
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   115
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   116
      val ml_platform =
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   117
        if (Platform.is_windows && arch_64) {
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   118
          if (check_dir(windows_64)) windows_64 else err(windows_64)
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   119
        }
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   120
        else if (Platform.is_windows && !arch_64) {
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   121
          if (check_dir(windows_32)) windows_32
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   122
          else platform_32  // x86-cygwin
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   123
        }
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   124
        else {
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   125
          val (platform, platform_name) =
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   126
            if (arch_64) (platform_64, "x86_64-" + platform_family)
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   127
            else (platform_32, "x86-" + platform_family)
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   128
          if (check_dir(platform)) platform else err(platform_name)
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   129
        }
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   130
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   131
      val ml_options =
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   132
        "-H " + heap + " --gcthreads " + threads +
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   133
        (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   134
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   135
      List(
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   136
        "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   137
        "ML_PLATFORM=" + quote(ml_platform),
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   138
        "ML_OPTIONS=" + quote(ml_options))
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   139
    }
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   140
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   141
    val thread_settings =
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   142
      List(
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   143
        "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   144
        "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   145
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   146
    File.append(etc_settings, "\n" +
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   147
      cat_lines(List(ml_settings, thread_settings).map(Library.terminate_lines(_))))
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   148
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   149
    if (more_settings.nonEmpty)
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   150
      File.append(etc_settings, "\n" + Library.terminate_lines(more_settings))
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   151
64032
wenzelm
parents: 64031
diff changeset
   152
wenzelm
parents: 64031
diff changeset
   153
    /* build */
wenzelm
parents: 64031
diff changeset
   154
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   155
    isabelle("components -a").check.print_if(verbose)
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   156
    isabelle("jedit -b" + (if (fresh) " -f" else "")).check.print_if(verbose)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   157
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   158
    isabelle("build " + File.bash_args(build_args))
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   159
  }
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   160
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   161
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   162
  /* command line entry point */
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   163
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   164
  def main(args: Array[String])
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   165
  {
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   166
    Command_Line.tool0 {
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   167
      var allow = false
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   168
      var components_base = ""
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   169
      var heap: Option[Int] = None
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   170
      var threads = default_threads
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   171
      var isabelle_identifier = default_isabelle_identifier
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   172
      var more_settings: List[String] = Nil
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   173
      var fresh = false
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   174
      var arch_64 = false
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   175
      var nonfree = false
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   176
      var rev = default_rev
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   177
      var verbose = false
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   178
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   179
      val getopts = Getopts("""
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   180
Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   181
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   182
  Options are:
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   183
    -A           allow irreversible cleanup of REPOSITORY clone (required)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   184
    -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   185
    -H HEAP      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   186
    -M THREADS   number of threads for Poly/ML RTS and Isabelle/ML (default: """ + default_threads + """)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   187
    -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   188
    -e TEXT      additional text for generated etc/settings
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   189
    -f           fresh build of Isabelle/Scala components (recommended)
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   190
    -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   191
    -n           include nonfree components
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   192
    -r REV       update to revision (default: """ + default_rev + """)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   193
    -v           verbose
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   194
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   195
  Build Isabelle sessions from the history of another REPOSITORY clone,
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   196
  passing ARGS directly to its isabelle build tool.
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   197
""",
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   198
        "A" -> (_ => allow = true),
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   199
        "C:" -> (arg => components_base = arg),
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   200
        "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   201
        "M:" -> (arg => threads = Value.Int.parse(arg)),
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   202
        "N:" -> (arg => isabelle_identifier = arg),
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   203
        "e:" -> (arg => more_settings = more_settings ::: List(arg)),
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   204
        "f" -> (_ => fresh = true),
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   205
        "m:" ->
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   206
          {
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   207
            case "32" | "x86" => arch_64 = false
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   208
            case "64" | "x86_64" => arch_64 = true
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   209
            case bad => error("Bad processor architecture: " + quote(bad))
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   210
          },
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   211
        "n" -> (_ => nonfree = true),
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   212
        "r:" -> (arg => rev = arg),
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   213
        "v" -> (_ => verbose = true))
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   214
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   215
      val more_args = getopts(args)
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   216
      val (root, build_args) =
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   217
        more_args match {
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   218
          case root :: build_args => (root, build_args)
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   219
          case _ => getopts.usage()
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   220
        }
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   221
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   222
      using(Mercurial.open_repository(Path.explode(root)))(hg =>
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   223
        {
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   224
          if (!allow)
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   225
            error("Repository " + hg + " will be cleaned thoroughly!\n" +
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   226
              "Provide option -A to allow this explicitly.")
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   227
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   228
          val res =
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   229
            build_history(hg, rev = rev, isabelle_identifier = isabelle_identifier,
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   230
              components_base = components_base, fresh = fresh, nonfree = nonfree,
64030
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   231
              threads = threads, arch_64 = arch_64,
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   232
              heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
04f9e1e9003a more options for generated settings;
wenzelm
parents: 64027
diff changeset
   233
              more_settings = more_settings, verbose = verbose, build_args = build_args)
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   234
          res.print
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   235
          if (!res.ok) sys.exit(res.rc)
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   236
        })
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   237
    }
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   238
  }
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   239
}