src/Pure/Admin/build_release.scala
author wenzelm
Mon, 22 Oct 2018 11:48:28 +0200
changeset 69176 63391630495f
parent 69175 561dc80624db
child 69177 300046d2ec60
permissions -rw-r--r--
tuned messages;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/build_release.scala
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
     3
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
     4
Build full Isabelle distribution from repository.
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
     5
*/
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
     6
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
     8
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
     9
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    10
object Build_Release
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    11
{
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    12
  /** release info **/
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    13
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    14
  sealed case class Bundle_Info(
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    15
    platform_family: String,
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    16
    platform_description: String,
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    17
    main: String,
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    18
    fallback: Option[String])
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    19
  {
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    20
    def names: List[String] = main :: fallback.toList
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    21
  }
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    22
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    23
  class Release private[Build_Release](
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    24
    val date: Date,
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    25
    val dist_name: String,
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    26
    val dist_dir: Path,
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    27
    val dist_version: String,
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    28
    val ident: String)
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    29
  {
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    30
    val isabelle_dir: Path = dist_dir + Path.explode(dist_name)
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    31
    val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    32
    val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    33
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    34
    val other_isabelle_identifier: String = dist_name + "-build"
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    35
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    36
    val bundle_infos: List[Bundle_Info] =
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    37
      List(Bundle_Info("linux", "Linux", dist_name + "_app.tar.gz", None),
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    38
        Bundle_Info("windows", "Windows", dist_name + ".exe", None),
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    39
        Bundle_Info("macos", "Mac OS X", dist_name + ".dmg", Some(dist_name + "_dmg.tar.gz")))
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    40
  }
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    41
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    42
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    43
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    44
  /** generated content **/
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    45
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    46
  /* patch release */
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    47
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    48
  private def change_file(dir: Path, name: String, f: String => String)
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    49
  {
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    50
    val file = dir + Path.explode(name)
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    51
    File.write(file, f(File.read(file)))
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    52
  }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    53
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
    54
  private val getsettings_file: String = "lib/scripts/getsettings"
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
    55
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
    56
  private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
    57
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    58
  def patch_release(release: Release, is_official: Boolean)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    59
  {
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    60
    val dir = release.isabelle_dir
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    61
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    62
    for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala"))
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    63
    {
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    64
      change_file(dir, name,
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    65
        s =>
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    66
          s.replaceAll("val is_identified = false", "val is_identified = true")
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    67
           .replaceAll("val is_official = false", "val is_official = " + is_official))
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    68
    }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    69
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
    70
    change_file(dir, getsettings_file,
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    71
      s =>
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    72
        s.replaceAll("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    73
         .replaceAll("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    74
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    75
    change_file(dir, "lib/html/library_index_header.template",
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    76
      s => s.replaceAll("""\{ISABELLE\}""", release.dist_name))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    77
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    78
    for {
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    79
      name <-
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    80
        List(
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    81
          "src/Pure/System/distribution.ML",
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    82
          "src/Pure/System/distribution.scala",
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    83
          "lib/Tools/version") }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    84
    {
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    85
      change_file(dir, name, s => s.replaceAll("repository version", release.dist_version))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    86
    }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    87
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    88
    change_file(dir, "README",
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    89
      s => s.replaceAll("some repository version of Isabelle", release.dist_version))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    90
  }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    91
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    92
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    93
  /* ANNOUNCE */
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    94
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    95
  def make_announce(release: Release)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    96
  {
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    97
    File.write(release.isabelle_dir + Path.explode("ANNOUNCE"),
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    98
"""
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    99
IMPORTANT NOTE
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   100
==============
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   101
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   102
This is a snapshot of Isabelle/""" + release.ident + """ from the repository.
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   103
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   104
""")
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   105
  }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   106
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   107
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   108
  /* NEWS */
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   109
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   110
  def make_news(other_isabelle: Other_Isabelle, dist_version: String)
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   111
  {
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   112
    val target = other_isabelle.isabelle_home + Path.explode("doc")
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   113
    val target_fonts = target + Path.explode("fonts")
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   114
    Isabelle_System.mkdirs(target_fonts)
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   115
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   116
    for (font <- other_isabelle.fonts(html = true))
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   117
      File.copy(font, target_fonts)
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   118
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   119
    HTML.write_document(target, "NEWS.html",
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   120
      List(HTML.title("NEWS (" + dist_version + ")")),
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   121
      List(
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   122
        HTML.chapter("NEWS"),
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   123
        HTML.source(
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   124
          Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS"))))))
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   125
  }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   126
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   127
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   128
  /* contrib */
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   129
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   130
  def make_contrib(dir: Path)
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   131
  {
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   132
    Isabelle_System.mkdirs(dir + Path.explode("contrib"))
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   133
    File.write(dir + Path.explode("contrib/README"),
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   134
"""This directory contains add-on components that contribute to the main
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   135
Isabelle distribution.  Separate licensing conditions apply, see each
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   136
directory individually.
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   137
""")
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   138
  }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   139
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   140
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   141
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   142
  /** build_release **/
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   143
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   144
  private def execute(dir: Path, script: String): Unit =
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   145
    Isabelle_System.bash(script, cwd = dir.file).check
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   146
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   147
  private def execute_tar(dir: Path, args: String): Unit =
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   148
    Isabelle_System.gnutar(args, cwd = dir.file).check
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   149
69170
6d28536481ad more portable tar_options;
wenzelm
parents: 69169
diff changeset
   150
  private def tar_options: String =
6d28536481ad more portable tar_options;
wenzelm
parents: 69169
diff changeset
   151
    if (Platform.is_macos) "--owner=root --group=staff" else "--owner=root --group=root"
6d28536481ad more portable tar_options;
wenzelm
parents: 69169
diff changeset
   152
66724
1e1f9f603385 "windows" application is always x86_64;
wenzelm
parents: 65838
diff changeset
   153
  private val default_platform_families = List("linux", "windows", "macos")
64204
db9ac35cae0d added option -p for platform families;
wenzelm
parents: 64203
diff changeset
   154
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   155
  def build_release(base_dir: Path,
64909
8007f10195af tuned signature;
wenzelm
parents: 64405
diff changeset
   156
    progress: Progress = No_Progress,
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   157
    rev: String = "",
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   158
    afp_rev: String = "",
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   159
    official_release: Boolean = false,
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   160
    proper_release_name: Option[String] = None,
64208
da9b04b8d204 clarified platform families vs. bundles;
wenzelm
parents: 64206
diff changeset
   161
    platform_families: List[String] = default_platform_families,
64211
1306a0e7fe81 explicit website directory;
wenzelm
parents: 64210
diff changeset
   162
    website: Option[Path] = None,
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   163
    build_library: Boolean = false,
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   164
    parallel_jobs: Int = 1,
69167
9456ba573729 tuned signature;
wenzelm
parents: 68755
diff changeset
   165
    remote_mac: String = ""): Release =
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   166
  {
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   167
    val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME"))
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   168
69167
9456ba573729 tuned signature;
wenzelm
parents: 68755
diff changeset
   169
    val release =
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   170
    {
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   171
      val date = Date.now()
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   172
      val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date))
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   173
      val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   175
      val version = proper_release_name orElse proper_string(rev) getOrElse "tip"
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   176
      val ident =
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   177
        try { hg.id(version) }
69176
63391630495f tuned messages;
wenzelm
parents: 69175
diff changeset
   178
        catch { case ERROR(_) => error("Bad repository version: " + version) }
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   179
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   180
      val dist_version =
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   181
        proper_release_name match {
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   182
          case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date)
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   183
          case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   184
        }
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   185
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   186
      new Release(date, dist_name, dist_dir, dist_version, ident)
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   187
    }
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   188
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   189
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   190
    /* make distribution */
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   191
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   192
    if (release.isabelle_archive.is_file) {
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   193
      progress.echo("### Release archive already exists: " + release.isabelle_archive.implode)
69175
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   194
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   195
      val archive_ident =
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   196
        Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   197
          {
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   198
            val getsettings = Path.explode(release.dist_name + "/" + getsettings_file)
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   199
            execute_tar(tmp_dir, "-xzf " +
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   200
              File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   201
            split_lines(File.read(tmp_dir + getsettings))
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   202
              .collectFirst({ case ISABELLE_ID(ident) => ident })
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   203
              .getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive))
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   204
          })
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   205
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   206
      if (release.ident != archive_ident) {
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   207
        error("Mismatch of release identification " + release.ident +
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   208
          " vs. archive " + archive_ident)
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   209
      }
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   210
    }
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   211
    else {
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   212
      progress.echo("### Producing release archive " + release.isabelle_archive.implode + " ...")
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   213
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   214
      Isabelle_System.mkdirs(release.dist_dir)
64221
407f69c4959f identify release;
wenzelm
parents: 64212
diff changeset
   215
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   216
      if (release.isabelle_dir.is_dir)
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   217
        error("Directory " + release.isabelle_dir + " already exists")
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   218
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   219
69176
63391630495f tuned messages;
wenzelm
parents: 69175
diff changeset
   220
      progress.echo("### Retrieving Mercurial repository version " + release.ident)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   221
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   222
      hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files")
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   223
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   224
      for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   225
        (release.isabelle_dir + Path.explode(name)).file.delete
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   226
      }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   227
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   228
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   229
      progress.echo("### Preparing distribution " + quote(release.dist_name))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   230
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   231
      patch_release(release, proper_release_name.isDefined && official_release)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   232
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   233
      if (proper_release_name.isEmpty) make_announce(release)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   234
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   235
      make_contrib(release.isabelle_dir)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   236
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   237
      execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   238
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   239
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   240
      /* build tools and documentation */
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   241
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   242
      val other_isabelle =
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   243
        Other_Isabelle(release.isabelle_dir,
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   244
          isabelle_identifier = release.other_isabelle_identifier,
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   245
          progress = progress)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   246
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   247
      other_isabelle.init_settings(
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   248
        (base_dir.absolute + Path.explode("contrib")).implode, nonfree = false, Nil)
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   249
      other_isabelle.resolve_components(echo = true)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   250
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   251
      try {
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   252
        val export_classpath =
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   253
          "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   254
        other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   255
        other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   256
      }
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   257
      catch { case ERROR(_) => error("Failed to build tools") }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   258
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   259
      try {
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   260
        other_isabelle.bash(
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   261
          "./bin/isabelle build_doc -a -s -j " + parallel_jobs, echo = true).check
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   262
      }
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   263
      catch { case ERROR(_) => error("Failed to build documentation") }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   264
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   265
      make_news(other_isabelle, release.dist_version)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   266
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   267
      for (name <- List("Admin", "browser_info", "heaps")) {
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   268
        Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   269
      }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   270
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   271
      other_isabelle.cleanup()
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   272
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   273
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   274
      progress.echo("### Creating distribution archive " + release.isabelle_archive)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   275
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   276
      def execute_dist_name(script: String): Unit =
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   277
        Isabelle_System.bash(script, cwd = release.dist_dir.file,
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   278
          env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   279
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   280
      execute_dist_name("""
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   281
set -e
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   282
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   283
chmod -R a+r "$DIST_NAME"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   284
chmod -R u+w "$DIST_NAME"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   285
chmod -R g=o "$DIST_NAME"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   286
find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   287
""")
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   288
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   289
      execute_tar(release.dist_dir, tar_options + " -czf " +
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   290
        File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   291
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   292
      execute_dist_name("""
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   293
set -e
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   294
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   295
mv "$DIST_NAME" "${DIST_NAME}-old"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   296
mkdir "$DIST_NAME"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   297
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   298
mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   299
  "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   300
mkdir "$DIST_NAME/doc"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   301
mv "${DIST_NAME}-old/doc/"*.pdf \
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   302
  "${DIST_NAME}-old/doc/"*.html \
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   303
  "${DIST_NAME}-old/doc/"*.css \
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   304
  "${DIST_NAME}-old/doc/fonts" \
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   305
  "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   306
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   307
rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   308
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   309
rm -rf "${DIST_NAME}-old"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   310
""")
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   311
    }
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   312
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   313
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   314
    /* make application bundles */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   315
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   316
    val bundle_infos =
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   317
      platform_families.map(family =>
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   318
        release.bundle_infos.find(info => info.platform_family == family) getOrElse
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   319
          error("Unknown platform family " + quote(family)))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   320
66730
wenzelm
parents: 66724
diff changeset
   321
    for (bundle_info <- bundle_infos) {
64361
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   322
      val bundle =
66730
wenzelm
parents: 66724
diff changeset
   323
        (if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main
69167
9456ba573729 tuned signature;
wenzelm
parents: 68755
diff changeset
   324
      val bundle_archive = release.dist_dir + Path.explode(bundle)
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   325
      if (bundle_archive.is_file)
64209
5d5701bed047 tuned messages;
wenzelm
parents: 64208
diff changeset
   326
        progress.echo("### Application bundle already exists: " + bundle_archive.implode)
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   327
      else {
64361
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   328
        progress.echo(
66730
wenzelm
parents: 66724
diff changeset
   329
          "\nApplication bundle for " + bundle_info.platform_family + ": " + bundle_archive.implode)
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   330
        progress.bash(
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   331
          "isabelle makedist_bundle " + File.bash_path(release.isabelle_archive) +
66730
wenzelm
parents: 66724
diff changeset
   332
            " " + Bash.string(bundle_info.platform_family) +
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64221
diff changeset
   333
            (if (remote_mac == "") "" else " " + Bash.string(remote_mac)),
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   334
          echo = true).check
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   335
      }
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   336
    }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   337
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   338
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   339
    /* minimal website */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   340
64361
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   341
    for (dir <- website) {
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   342
      val website_platform_bundles =
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   343
        for {
66730
wenzelm
parents: 66724
diff changeset
   344
          bundle_info <- bundle_infos
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   345
          bundle <- bundle_info.names.find(name => (release.dist_dir + Path.explode(name)).is_file)
66730
wenzelm
parents: 66724
diff changeset
   346
        } yield (bundle, bundle_info)
64206
cb98e0e5f1e5 website index for existing bundles;
wenzelm
parents: 64205
diff changeset
   347
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   348
      val afp_link =
66854
wenzelm
parents: 66730
diff changeset
   349
        HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev))
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   350
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   351
      HTML.write_document(dir, "index.html",
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   352
        List(HTML.title(release.dist_name)),
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   353
        List(
69175
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   354
          HTML.chapter(release.dist_name + " (" + release.ident + ")"),
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   355
          HTML.itemize(
66730
wenzelm
parents: 66724
diff changeset
   356
            website_platform_bundles.map({ case (bundle, bundle_info) =>
wenzelm
parents: 66724
diff changeset
   357
              List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) :::
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   358
        (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link)))))
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   359
64361
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   360
      for ((bundle, _) <- website_platform_bundles)
69167
9456ba573729 tuned signature;
wenzelm
parents: 68755
diff changeset
   361
        File.copy(release.dist_dir + Path.explode(bundle), dir)
64361
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   362
    }
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   363
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   364
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   365
    /* HTML library */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   366
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   367
    if (build_library) {
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   368
      if (release.isabelle_library_archive.is_file) {
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   369
        progress.echo(
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   370
          "### Library archive already exists: " + release.isabelle_library_archive.implode)
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   371
      }
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   372
      else {
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   373
        Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   374
          {
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   375
            val name = release.dist_name
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   376
            val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY")
69167
9456ba573729 tuned signature;
wenzelm
parents: 68755
diff changeset
   377
            val bundle = release.dist_dir + Path.explode(name + "_" + platform + ".tar.gz")
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   378
            execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   379
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   380
            val other_isabelle =
67045
6c94f749410a tuned signature;
wenzelm
parents: 66923
diff changeset
   381
              Other_Isabelle(tmp_dir + Path.explode(name),
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   382
                isabelle_identifier = release.other_isabelle_identifier, progress = progress)
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   383
68755
67d6f1708ea4 enforce ML_system_64: more robust as cold build, without command_timings;
wenzelm
parents: 67045
diff changeset
   384
            Isabelle_System.mkdirs(other_isabelle.etc)
67d6f1708ea4 enforce ML_system_64: more robust as cold build, without command_timings;
wenzelm
parents: 67045
diff changeset
   385
            File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
67d6f1708ea4 enforce ML_system_64: more robust as cold build, without command_timings;
wenzelm
parents: 67045
diff changeset
   386
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   387
            other_isabelle.bash("bin/isabelle build -j " + parallel_jobs +
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   388
                " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   389
                " -s -c -a -d '~~/src/Benchmarks'", echo = true).check
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   390
            other_isabelle.isabelle_home_user.file.delete
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   391
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   392
            execute(tmp_dir, "chmod -R a+r " + Bash.string(name))
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   393
            execute(tmp_dir, "chmod -R g=o " + Bash.string(name))
69170
6d28536481ad more portable tar_options;
wenzelm
parents: 69169
diff changeset
   394
            execute_tar(tmp_dir,
6d28536481ad more portable tar_options;
wenzelm
parents: 69169
diff changeset
   395
              tar_options + " -czf " + File.bash_path(release.isabelle_library_archive) +
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   396
              " " + Bash.string(name + "/browser_info"))
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   397
          })
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   398
      }
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   399
    }
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   400
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   401
    release
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   402
  }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   403
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   404
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   405
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   406
  /** command line entry point **/
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   407
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   408
  def main(args: Array[String])
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   409
  {
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   410
    Command_Line.tool0 {
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   411
      var afp_rev = ""
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   412
      var remote_mac = ""
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   413
      var official_release = false
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   414
      var proper_release_name: Option[String] = None
64211
1306a0e7fe81 explicit website directory;
wenzelm
parents: 64210
diff changeset
   415
      var website: Option[Path] = None
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   416
      var parallel_jobs = 1
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   417
      var build_library = false
64208
da9b04b8d204 clarified platform families vs. bundles;
wenzelm
parents: 64206
diff changeset
   418
      var platform_families = default_platform_families
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   419
      var rev = ""
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   420
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   421
      val getopts = Getopts("""
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   422
Usage: Admin/build_release [OPTIONS] BASE_DIR
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   423
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   424
  Options are:
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   425
    -A REV       corresponding AFP changeset id
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   426
    -M USER@HOST remote Mac OS X for dmg build
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   427
    -O           official release (not release-candidate)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   428
    -R RELEASE   proper release with name
64211
1306a0e7fe81 explicit website directory;
wenzelm
parents: 64210
diff changeset
   429
    -W WEBSITE   produce minimal website in given directory
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   430
    -j INT       maximum number of parallel jobs (default 1)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   431
    -l           build library
65067
8bc9de2278c0 tuned message;
wenzelm
parents: 64936
diff changeset
   432
    -p NAMES     platform families (default: """ + default_platform_families.mkString(",") + """)
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   433
    -r REV       Mercurial changeset id (default: RELEASE or tip)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   434
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   435
  Build Isabelle release in base directory, using the local repository clone.
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   436
""",
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   437
        "A:" -> (arg => afp_rev = arg),
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   438
        "M:" -> (arg => remote_mac = arg),
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   439
        "O" -> (_ => official_release = true),
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   440
        "R:" -> (arg => proper_release_name = Some(arg)),
64211
1306a0e7fe81 explicit website directory;
wenzelm
parents: 64210
diff changeset
   441
        "W:" -> (arg => website = Some(Path.explode(arg))),
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   442
        "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   443
        "l" -> (_ => build_library = true),
66923
wenzelm
parents: 66910
diff changeset
   444
        "p:" -> (arg => platform_families = space_explode(',', arg)),
64204
db9ac35cae0d added option -p for platform families;
wenzelm
parents: 64203
diff changeset
   445
        "r:" -> (arg => rev = arg))
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   446
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   447
      val more_args = getopts(args)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   448
      val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   449
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   450
      val progress = new Console_Progress()
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   451
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   452
      build_release(Path.explode(base_dir), progress = progress, rev = rev, afp_rev = afp_rev,
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   453
        official_release = official_release, proper_release_name = proper_release_name,
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   454
        website = website,
64204
db9ac35cae0d added option -p for platform families;
wenzelm
parents: 64203
diff changeset
   455
        platform_families =
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   456
          if (platform_families.isEmpty) default_platform_families
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   457
          else platform_families,
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   458
        build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   459
    }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   460
  }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   461
}