src/Pure/Admin/build_release.scala
author wenzelm
Wed, 10 Apr 2019 13:45:49 +0200
changeset 70103 a6236d5a89ae
parent 70102 e48ffba6b557
child 70206 c7fa2b7d2c8a
permissions -rw-r--r--
tuned message;
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(
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
    15
    platform: Platform.Family.Value,
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    16
    platform_description: String,
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
    17
    name: String)
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    18
  {
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
    19
    def path: Path = Path.explode(name)
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    20
  }
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    21
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    22
  class Release private[Build_Release](
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
    23
    progress: Progress,
69174
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
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
    34
    def other_isabelle(dir: Path): Other_Isabelle =
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
    35
      Other_Isabelle(dir + Path.explode(dist_name),
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
    36
        isabelle_identifier = dist_name + "-build",
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
    37
        progress = progress)
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    38
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
    39
    def bundle_info(platform: Platform.Family.Value): Bundle_Info =
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
    40
      platform match {
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
    41
        case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
    42
        case Platform.Family.macos => Bundle_Info(platform, "Mac OS X", dist_name + "_macos.tar.gz")
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
    43
        case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
69177
300046d2ec60 tuned signature;
wenzelm
parents: 69176
diff changeset
    44
      }
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    45
  }
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    46
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    47
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    48
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    49
  /** generated content **/
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    50
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    51
  /* patch release */
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
  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
    54
  {
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    55
    val file = dir + Path.explode(name)
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    56
    File.write(file, f(File.read(file)))
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    57
  }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    58
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
    59
  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
    60
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
    61
  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
    62
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    63
  def patch_release(release: Release, is_official: Boolean)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    64
  {
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    65
    val dir = release.isabelle_dir
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    66
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    67
    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
    68
    {
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    69
      change_file(dir, name,
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    70
        s =>
69392
wenzelm
parents: 69391
diff changeset
    71
          s.replaceAllLiterally("val is_identified = false", "val is_identified = true")
wenzelm
parents: 69391
diff changeset
    72
           .replaceAllLiterally("val is_official = false", "val is_official = " + is_official))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    73
    }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    74
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
    75
    change_file(dir, getsettings_file,
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    76
      s =>
69392
wenzelm
parents: 69391
diff changeset
    77
        s.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
wenzelm
parents: 69391
diff changeset
    78
         .replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"",
wenzelm
parents: 69391
diff changeset
    79
            "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    80
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    81
    change_file(dir, "lib/html/library_index_header.template",
69392
wenzelm
parents: 69391
diff changeset
    82
      s => s.replaceAllLiterally("{ISABELLE}", release.dist_name))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    83
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    84
    for {
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    85
      name <-
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    86
        List(
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    87
          "src/Pure/System/distribution.ML",
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    88
          "src/Pure/System/distribution.scala",
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    89
          "lib/Tools/version") }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    90
    {
69392
wenzelm
parents: 69391
diff changeset
    91
      change_file(dir, name,
wenzelm
parents: 69391
diff changeset
    92
        s => s.replaceAllLiterally("repository version", release.dist_version))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    93
    }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    94
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    95
    change_file(dir, "README",
69392
wenzelm
parents: 69391
diff changeset
    96
      s => s.replaceAllLiterally("some repository version of Isabelle", release.dist_version))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
    97
  }
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
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   100
  /* ANNOUNCE */
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
  def make_announce(release: Release)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   103
  {
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   104
    File.write(release.isabelle_dir + Path.explode("ANNOUNCE"),
69168
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
IMPORTANT NOTE
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
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   109
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
   110
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
  }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   113
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   114
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   115
  /* NEWS */
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   116
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   117
  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
   118
  {
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   119
    val target = other_isabelle.isabelle_home + Path.explode("doc")
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   120
    val target_fonts = target + Path.explode("fonts")
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   121
    Isabelle_System.mkdirs(target_fonts)
69360
dc9a39c3f75d more explicit Isabelle_Fonts.Entry;
wenzelm
parents: 69178
diff changeset
   122
    other_isabelle.copy_fonts(target_fonts)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   123
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   124
    HTML.write_document(target, "NEWS.html",
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   125
      List(HTML.title("NEWS (" + dist_version + ")")),
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   126
      List(
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   127
        HTML.chapter("NEWS"),
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   128
        HTML.source(
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   129
          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
   130
  }
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
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   133
  /* bundled components */
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   134
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   135
  class Bundled(platform: Option[Platform.Family.Value] = None)
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   136
  {
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   137
    def detect(s: String): Boolean =
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   138
      s.startsWith("#bundled") && !s.startsWith("#bundled ")
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   139
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   140
    def apply(name: String): String =
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   141
      "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   142
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   143
    private val Pattern1 = ("""^#bundled:(.*)$""").r
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   144
    private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   145
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   146
    def unapply(s: String): Option[String] =
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   147
      s match {
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   148
        case Pattern1(name) => Some(name)
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   149
        case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name)
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   150
        case _ => None
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   151
      }
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   152
  }
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   153
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   154
  def record_bundled_components(dir: Path)
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   155
  {
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   156
    val catalogs =
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   157
      List("main", "bundled").map((_, new Bundled())) :::
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   158
      default_platform_families.flatMap(platform =>
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   159
        List(platform.toString, "bundled-" + platform.toString).
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   160
          map((_, new Bundled(platform = Some(platform)))))
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   161
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   162
    File.append(Components.components(dir),
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   163
      terminate_lines("#bundled components" ::
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   164
        (for {
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   165
          (catalog, bundled) <- catalogs.iterator
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   166
          val path = Components.admin(dir) + Path.basic(catalog)
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   167
          if path.is_file
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   168
          line <- split_lines(File.read(path))
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   169
          if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   170
        } yield bundled(line)).toList))
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   171
  }
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   172
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   173
  def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) =
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   174
  {
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   175
    val Bundled = new Bundled(platform = Some(platform))
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   176
    val components =
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   177
      for {
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   178
        Bundled(name) <- Components.read_components(dir)
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   179
        if !name.startsWith("jedit_build")
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   180
      } yield name
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   181
    val jdk_component =
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   182
      components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   183
    (components, jdk_component)
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   184
  }
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   185
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   186
  def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String])
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   187
  {
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   188
    def contrib_name(name: String): String =
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   189
      Components.contrib(name = name).implode
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   190
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   191
    val Bundled = new Bundled(platform = Some(platform))
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   192
    Components.write_components(dir,
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   193
      Components.read_components(dir).flatMap(line =>
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   194
        line match {
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   195
          case Bundled(name) =>
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   196
            if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   197
            else None
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   198
          case _ => if (Bundled.detect(line)) None else Some(line)
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   199
        }) ::: more_names.map(contrib_name(_)))
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   200
  }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   201
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   202
  def make_contrib(dir: Path)
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   203
  {
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   204
    Isabelle_System.mkdirs(Components.contrib(dir))
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   205
    File.write(Components.contrib(dir, "README"),
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   206
"""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
   207
Isabelle distribution.  Separate licensing conditions apply, see each
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   208
directory individually.
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   209
""")
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   210
  }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   211
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   212
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   213
70099
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   214
  /** build release **/
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   215
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   216
  private def execute(dir: Path, script: String): Unit =
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   217
    Isabelle_System.bash(script, cwd = dir.file).check
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   218
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   219
  private def execute_tar(dir: Path, args: String): Unit =
69425
94f6ca69d983 clarified gnutar options: more uniform owner;
wenzelm
parents: 69424
diff changeset
   220
    Isabelle_System.gnutar(args, dir = dir).check
69170
6d28536481ad more portable tar_options;
wenzelm
parents: 69169
diff changeset
   221
70099
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   222
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   223
  /* build heaps on remote server */
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   224
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   225
  private def remote_build_heaps(
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   226
    options: Options,
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   227
    platform: Platform.Family.Value,
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   228
    build_sessions: List[String],
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   229
    local_dir: Path)
70099
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   230
  {
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   231
    val server_option = "build_release_server_" + platform.toString
70099
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   232
    options.string(server_option) match {
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   233
      case SSH.Target(user, host) =>
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   234
        using(SSH.open_session(options, host = host, user = user))(ssh =>
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   235
        {
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   236
          Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar =>
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   237
          {
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   238
            execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   239
            ssh.with_tmp_dir(remote_dir =>
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   240
            {
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   241
              val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   242
              ssh.write_file(remote_tmp_tar, local_tmp_tar)
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   243
              val remote_commands =
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   244
                List(
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   245
                  "cd " + File.bash_path(remote_dir),
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   246
                  "tar -xf tmp.tar",
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   247
                  "./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   248
                  "tar -cf tmp.tar heaps")
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   249
              ssh.execute(remote_commands.mkString(" && ")).check
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   250
              ssh.read_file(remote_tmp_tar, local_tmp_tar)
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   251
            })
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   252
            execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   253
          })
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   254
        })
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   255
      case s => error("Bad " + server_option + ": " + quote(s))
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   256
    }
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   257
  }
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   258
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   259
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   260
  /* main */
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   261
69415
99c3529c31d0 clarified error;
wenzelm
parents: 69414
diff changeset
   262
  private val default_platform_families: List[Platform.Family.Value] =
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   263
    List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
64204
db9ac35cae0d added option -p for platform families;
wenzelm
parents: 64203
diff changeset
   264
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   265
  def build_release(base_dir: Path,
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   266
    options: Options,
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69432
diff changeset
   267
    components_base: Path = Components.default_components_base,
64909
8007f10195af tuned signature;
wenzelm
parents: 64405
diff changeset
   268
    progress: Progress = No_Progress,
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   269
    rev: String = "",
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   270
    afp_rev: String = "",
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   271
    official_release: Boolean = false,
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   272
    proper_release_name: Option[String] = None,
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   273
    platform_families: List[Platform.Family.Value] = default_platform_families,
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   274
    more_components: List[Path] = Nil,
64211
1306a0e7fe81 explicit website directory;
wenzelm
parents: 64210
diff changeset
   275
    website: Option[Path] = None,
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   276
    build_sessions: List[String] = Nil,
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   277
    build_library: Boolean = false,
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
   278
    parallel_jobs: Int = 1): Release =
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   279
  {
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   280
    val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME"))
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   281
69167
9456ba573729 tuned signature;
wenzelm
parents: 68755
diff changeset
   282
    val release =
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   283
    {
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   284
      val date = Date.now()
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   285
      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
   286
      val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   287
69414
eab0d3108b46 clarified defaults: explicit "rev" takes precedence;
wenzelm
parents: 69413
diff changeset
   288
      val version = proper_string(rev) orElse proper_release_name getOrElse "tip"
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   289
      val ident =
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   290
        try { hg.id(version) }
69176
63391630495f tuned messages;
wenzelm
parents: 69175
diff changeset
   291
        catch { case ERROR(_) => error("Bad repository version: " + version) }
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   292
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   293
      val dist_version =
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   294
        proper_release_name match {
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   295
          case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date)
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   296
          case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   297
        }
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   298
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   299
      new Release(progress, 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
   300
    }
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   301
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   302
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   303
    /* make distribution */
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   304
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   305
    if (release.isabelle_archive.is_file) {
69400
wenzelm
parents: 69397
diff changeset
   306
      progress.echo_warning("Release archive already exists: " + release.isabelle_archive)
69175
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   307
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   308
      val archive_ident =
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   309
        Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   310
          {
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   311
            val getsettings = Path.explode(release.dist_name + "/" + getsettings_file)
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   312
            execute_tar(tmp_dir, "-xzf " +
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   313
              File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   314
            split_lines(File.read(tmp_dir + getsettings))
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   315
              .collectFirst({ case ISABELLE_ID(ident) => ident })
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   316
              .getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive))
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   317
          })
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   318
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   319
      if (release.ident != archive_ident) {
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   320
        error("Mismatch of release identification " + release.ident +
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   321
          " vs. archive " + archive_ident)
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   322
      }
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   323
    }
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   324
    else {
69400
wenzelm
parents: 69397
diff changeset
   325
      progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...")
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   326
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   327
      Isabelle_System.mkdirs(release.dist_dir)
64221
407f69c4959f identify release;
wenzelm
parents: 64212
diff changeset
   328
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   329
      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
   330
        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
   331
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   332
69400
wenzelm
parents: 69397
diff changeset
   333
      progress.echo_warning("Retrieving Mercurial repository version " + release.ident)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   334
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   335
      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
   336
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   337
      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
   338
        (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
   339
      }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   340
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   341
69400
wenzelm
parents: 69397
diff changeset
   342
      progress.echo_warning("Preparing distribution " + quote(release.dist_name))
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   343
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   344
      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
   345
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   346
      if (proper_release_name.isEmpty) make_announce(release)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   347
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   348
      make_contrib(release.isabelle_dir)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   349
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   350
      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
   351
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   352
      record_bundled_components(release.isabelle_dir)
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   353
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   354
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   355
      /* build tools and documentation */
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   356
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   357
      val other_isabelle = release.other_isabelle(release.dist_dir)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   358
69388
fc58534bc475 clarified component settings;
wenzelm
parents: 69387
diff changeset
   359
      other_isabelle.init_settings(
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69432
diff changeset
   360
        other_isabelle.init_components(components_base = components_base, catalogs = List("main")))
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   361
      other_isabelle.resolve_components(echo = true)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   362
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   363
      try {
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   364
        val export_classpath =
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   365
          "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
   366
        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
   367
        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
   368
      }
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   369
      catch { case ERROR(_) => error("Failed to build tools") }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   370
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   371
      try {
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   372
        other_isabelle.bash(
69873
6ebe97815275 proper option (amending cc0b3e177b49);
wenzelm
parents: 69789
diff changeset
   373
          "./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   374
      }
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   375
      catch { case ERROR(_) => error("Failed to build documentation") }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   376
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   377
      make_news(other_isabelle, release.dist_version)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   378
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   379
      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
   380
        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
   381
      }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   382
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   383
      other_isabelle.cleanup()
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   384
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   385
69400
wenzelm
parents: 69397
diff changeset
   386
      progress.echo_warning("Creating distribution archive " + release.isabelle_archive)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   387
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   388
      def execute_dist_name(script: String): Unit =
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   389
        Isabelle_System.bash(script, cwd = release.dist_dir.file,
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   390
          env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   391
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   392
      execute_dist_name("""
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   393
set -e
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   394
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   395
chmod -R a+r "$DIST_NAME"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   396
chmod -R u+w "$DIST_NAME"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   397
chmod -R g=o "$DIST_NAME"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   398
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
   399
""")
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   400
69425
94f6ca69d983 clarified gnutar options: more uniform owner;
wenzelm
parents: 69424
diff changeset
   401
      execute_tar(release.dist_dir, "-czf " +
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   402
        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
   403
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   404
      execute_dist_name("""
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   405
set -e
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   406
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   407
mv "$DIST_NAME" "${DIST_NAME}-old"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   408
mkdir "$DIST_NAME"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   409
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   410
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
   411
  "${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
   412
mkdir "$DIST_NAME/doc"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   413
mv "${DIST_NAME}-old/doc/"*.pdf \
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   414
  "${DIST_NAME}-old/doc/"*.html \
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   415
  "${DIST_NAME}-old/doc/"*.css \
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   416
  "${DIST_NAME}-old/doc/fonts" \
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   417
  "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   418
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   419
rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   420
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   421
rm -rf "${DIST_NAME}-old"
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   422
""")
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   423
    }
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   424
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   425
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   426
    /* make application bundles */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   427
69177
300046d2ec60 tuned signature;
wenzelm
parents: 69176
diff changeset
   428
    val bundle_infos = platform_families.map(release.bundle_info)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   429
66730
wenzelm
parents: 66724
diff changeset
   430
    for (bundle_info <- bundle_infos) {
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
   431
      val bundle_archive = release.dist_dir + bundle_info.path
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   432
      val isabelle_name = release.dist_name
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   433
      val platform = bundle_info.platform
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   434
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   435
      progress.echo("\nApplication bundle for " + platform)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   436
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   437
      Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   438
      {
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   439
        // release archive
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   440
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   441
        execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   442
        val other_isabelle = release.other_isabelle(tmp_dir)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   443
        val isabelle_target = other_isabelle.isabelle_home
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   444
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   445
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   446
        // bundled components
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   447
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   448
        progress.echo("Bundled components:")
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   449
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   450
        val contrib_dir = Components.contrib(isabelle_target)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   451
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   452
        val (bundled_components, jdk_component) =
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   453
          get_bundled_components(isabelle_target, platform)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   454
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   455
        Components.resolve(components_base, bundled_components,
70102
e48ffba6b557 retain copy of required components;
wenzelm
parents: 70101
diff changeset
   456
          target_dir = Some(contrib_dir),
e48ffba6b557 retain copy of required components;
wenzelm
parents: 70101
diff changeset
   457
          copy_dir = Some(release.dist_dir + Path.explode("contrib")),
e48ffba6b557 retain copy of required components;
wenzelm
parents: 70101
diff changeset
   458
          progress = progress)
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   459
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   460
        val more_components_names =
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   461
          more_components.map(Components.unpack(contrib_dir, _, progress = progress))
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   462
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   463
        Components.purge(contrib_dir, platform)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   464
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   465
        activate_components(isabelle_target, platform, more_components_names)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   466
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   467
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   468
        // Java parameters
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   469
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   470
        val java_options_title = "# Java runtime options"
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   471
        val java_options: List[String] =
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   472
          (for {
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   473
            variable <-
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   474
              List(
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   475
                "ISABELLE_JAVA_SYSTEM_OPTIONS",
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   476
                "JEDIT_JAVA_SYSTEM_OPTIONS",
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   477
                "JEDIT_JAVA_OPTIONS")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   478
            opt <- Word.explode(other_isabelle.getenv(variable))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   479
          } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   480
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   481
        val classpath: List[Path] =
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   482
        {
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   483
          val base = isabelle_target.absolute
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   484
          Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   485
          {
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   486
            val abs_path = path.absolute
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   487
            File.relative_path(base, abs_path) match {
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   488
              case Some(rel_path) => rel_path
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   489
              case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   490
            }
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   491
          }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   492
        }
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   493
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   494
        val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   495
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   496
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   497
        // build heaps
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   498
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   499
        if (build_sessions.nonEmpty) {
70103
a6236d5a89ae tuned message;
wenzelm
parents: 70102
diff changeset
   500
          progress.echo("Building heaps ...")
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   501
          remote_build_heaps(options, platform, build_sessions, isabelle_target)
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   502
        }
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   503
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   504
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   505
        // application bundling
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   506
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   507
        platform match {
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   508
          case Platform.Family.linux =>
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   509
            File.write(isabelle_target + Path.explode(isabelle_name + ".options"),
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   510
              terminate_lines(java_options_title :: java_options))
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   511
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   512
            val isabelle_run = isabelle_target + Path.explode(isabelle_name + ".run")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   513
            File.write(isabelle_run,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   514
              File.read(Path.explode("~~/Admin/Linux/Isabelle.run"))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   515
                .replaceAllLiterally("{CLASSPATH}",
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   516
                  classpath.map("$ISABELLE_HOME/" + _).mkString(":"))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   517
                .replaceAllLiterally("/jdk/", "/" + jdk_component + "/"))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   518
            File.set_executable(isabelle_run, true)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   519
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   520
            val linux_app = isabelle_target + Path.explode("contrib/linux_app")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   521
            File.move(linux_app + Path.explode("Isabelle"),
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   522
              isabelle_target + Path.explode(isabelle_name))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   523
            Isabelle_System.rm_tree(linux_app)
69417
wenzelm
parents: 69415
diff changeset
   524
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   525
            val archive_name = isabelle_name + "_linux.tar.gz"
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   526
            progress.echo("Packaging " + archive_name + " ...")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   527
            execute_tar(tmp_dir,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   528
              "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   529
              Bash.string(isabelle_name))
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   530
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
   531
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   532
          case Platform.Family.macos =>
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   533
            File.write(isabelle_target + jedit_props,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   534
              File.read(isabelle_target + jedit_props)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   535
                .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   536
                .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   537
                .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   538
                .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
69417
wenzelm
parents: 69415
diff changeset
   539
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   540
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   541
            // MacOS application bundle
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   542
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   543
            File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   544
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   545
            val isabelle_app = Path.explode(isabelle_name + ".app")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   546
            val app_dir = tmp_dir + isabelle_app
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   547
            File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   548
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   549
            val app_contents = app_dir + Path.explode("Contents")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   550
            val app_resources = app_contents + Path.explode("Resources")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   551
            File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   552
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   553
            File.write(app_contents + Path.explode("Info.plist"),
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   554
              File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   555
                .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   556
                .replaceAllLiterally("{JAVA_OPTIONS}",
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   557
                  terminate_lines(java_options.map(opt => "<string>" + opt + "</string>"))))
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   558
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   559
            for (cp <- classpath) {
69417
wenzelm
parents: 69415
diff changeset
   560
              File.link(
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   561
                Path.explode("../Resources/" + isabelle_name + "/") + cp,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   562
                app_contents + Path.explode("Java"),
69417
wenzelm
parents: 69415
diff changeset
   563
                force = true)
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   564
            }
69402
61f4c406d727 more direct File.link operation: avoid external process;
wenzelm
parents: 69401
diff changeset
   565
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   566
            File.link(
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   567
              Path.explode("../Resources/" + isabelle_name + "/contrib/" +
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   568
                jdk_component + "/x86_64-darwin"),
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   569
              app_contents + Path.explode("PlugIns/bundled.jdk"),
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   570
              force = true)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   571
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   572
            File.link(
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   573
              Path.explode("../../Info.plist"),
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   574
              app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"),
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   575
              force = true)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   576
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   577
            File.link(
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   578
              Path.explode("Contents/Resources/" + isabelle_name),
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   579
              app_dir + Path.explode("Isabelle"),
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   580
              force = true)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   581
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   582
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   583
            // application archive
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   584
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   585
            val archive_name = isabelle_name + "_macos.tar.gz"
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   586
            progress.echo("Packaging " + archive_name + " ...")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   587
            execute_tar(tmp_dir,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   588
              "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   589
              File.bash_path(isabelle_app))
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
   590
69417
wenzelm
parents: 69415
diff changeset
   591
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   592
          case Platform.Family.windows =>
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   593
            File.write(isabelle_target + jedit_props,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   594
              File.read(isabelle_target + jedit_props)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   595
                .replaceAll("lookAndFeel=.*",
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   596
                  "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   597
                .replaceAll("foldPainter=.*", "foldPainter=Square"))
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   598
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   599
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   600
            // application launcher
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   601
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   602
            File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   603
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   604
            val app_template = Path.explode("~~/Admin/Windows/launch4j")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   605
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   606
            File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   607
              (java_options_title :: java_options).map(_ + "\r\n").mkString)
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   608
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   609
            val isabelle_xml = Path.explode("isabelle.xml")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   610
            val isabelle_exe = Path.explode(isabelle_name + ".exe")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   611
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   612
            File.write(tmp_dir + isabelle_xml,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   613
              File.read(app_template + isabelle_xml)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   614
                .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   615
                .replaceAllLiterally("{OUTFILE}",
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   616
                  File.platform_path(isabelle_target + isabelle_exe))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   617
                .replaceAllLiterally("{ICON}",
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   618
                  File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   619
                .replaceAllLiterally("{SPLASH}",
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   620
                  File.platform_path(app_template + Path.explode("isabelle.bmp")))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   621
                .replaceAllLiterally("{CLASSPATH}",
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   622
                  cat_lines(classpath.map(cp =>
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   623
                    "    <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>")))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   624
                .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   625
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   626
            execute(tmp_dir,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   627
              "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   628
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   629
            File.copy(app_template + Path.explode("manifest.xml"),
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   630
              isabelle_target + isabelle_exe.ext("manifest"))
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   631
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   632
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   633
            // Cygwin setup
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   634
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   635
            val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   636
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   637
            File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   638
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   639
            val cygwin_mirror =
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   640
              File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   641
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   642
            val cygwin_bat = Path.explode("Cygwin-Setup.bat")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   643
            File.write(isabelle_target + cygwin_bat,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   644
              File.read(cygwin_template + cygwin_bat)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   645
                .replaceAllLiterally("{MIRROR}", cygwin_mirror))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   646
            File.set_executable(isabelle_target + cygwin_bat, true)
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   647
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   648
            for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   649
              val path = Path.explode(name)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   650
              File.copy(cygwin_template + path,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   651
                isabelle_target + Path.explode("contrib/cygwin") + path)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   652
            }
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   653
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   654
            execute(isabelle_target,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   655
              """find . -type f -not -name "*.exe" -not -name "*.dll" """ +
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   656
              (if (Platform.is_macos) "-perm +100" else "-executable") +
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   657
              " -print0 > contrib/cygwin/isabelle/executables")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   658
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   659
            execute(isabelle_target,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   660
              """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   661
              """> contrib/cygwin/isabelle/symlinks""")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   662
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   663
            execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   664
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   665
            File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   666
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   667
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   668
            // executable archive (self-extracting 7z)
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   669
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   670
            val archive_name = isabelle_name + ".7z"
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   671
            val exe_archive = tmp_dir + Path.explode(archive_name)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   672
            exe_archive.file.delete
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   673
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   674
            progress.echo("Packaging " + archive_name + " ...")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   675
            execute(tmp_dir,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   676
              "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   677
            if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   678
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   679
            val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   680
            val sfx_txt =
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   681
              File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")).
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   682
                replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   683
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   684
            Bytes.write(release.dist_dir + isabelle_exe,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   685
              Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   686
            File.set_executable(release.dist_dir + isabelle_exe, true)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   687
        }
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   688
      })
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   689
      progress.echo("DONE")
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   690
    }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   691
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   692
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   693
    /* minimal website */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   694
64361
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   695
    for (dir <- website) {
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   696
      val website_platform_bundles =
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   697
        for {
66730
wenzelm
parents: 66724
diff changeset
   698
          bundle_info <- bundle_infos
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
   699
          if (release.dist_dir + bundle_info.path).is_file
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
   700
        } yield (bundle_info.name, bundle_info)
64206
cb98e0e5f1e5 website index for existing bundles;
wenzelm
parents: 64205
diff changeset
   701
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   702
      val afp_link =
70046
c37525278ae2 proper URL;
wenzelm
parents: 69873
diff changeset
   703
        HTML.link(AFP.repos_source + "/rev/" + 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
   704
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   705
      HTML.write_document(dir, "index.html",
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   706
        List(HTML.title(release.dist_name)),
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   707
        List(
69175
561dc80624db more robust: check archive ident;
wenzelm
parents: 69174
diff changeset
   708
          HTML.chapter(release.dist_name + " (" + release.ident + ")"),
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   709
          HTML.itemize(
66730
wenzelm
parents: 66724
diff changeset
   710
            website_platform_bundles.map({ case (bundle, bundle_info) =>
wenzelm
parents: 66724
diff changeset
   711
              List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) :::
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   712
        (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
   713
64361
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   714
      for ((bundle, _) <- website_platform_bundles)
69167
9456ba573729 tuned signature;
wenzelm
parents: 68755
diff changeset
   715
        File.copy(release.dist_dir + Path.explode(bundle), dir)
64361
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   716
    }
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   717
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   718
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   719
    /* HTML library */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   720
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   721
    if (build_library) {
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   722
      if (release.isabelle_library_archive.is_file) {
69400
wenzelm
parents: 69397
diff changeset
   723
        progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   724
      }
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   725
      else {
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   726
        Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   727
          {
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   728
            val bundle =
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   729
              release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz")
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   730
            execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   731
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   732
            val other_isabelle = release.other_isabelle(tmp_dir)
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   733
68755
67d6f1708ea4 enforce ML_system_64: more robust as cold build, without command_timings;
wenzelm
parents: 67045
diff changeset
   734
            Isabelle_System.mkdirs(other_isabelle.etc)
67d6f1708ea4 enforce ML_system_64: more robust as cold build, without command_timings;
wenzelm
parents: 67045
diff changeset
   735
            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
   736
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   737
            other_isabelle.bash("bin/isabelle build -j " + parallel_jobs +
69406
wenzelm
parents: 69405
diff changeset
   738
              " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
69873
6ebe97815275 proper option (amending cc0b3e177b49);
wenzelm
parents: 69789
diff changeset
   739
              " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   740
            other_isabelle.isabelle_home_user.file.delete
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   741
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   742
            execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   743
            execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
69425
94f6ca69d983 clarified gnutar options: more uniform owner;
wenzelm
parents: 69424
diff changeset
   744
            execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) +
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   745
              " " + Bash.string(release.dist_name + "/browser_info"))
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   746
          })
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   747
      }
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   748
    }
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   749
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   750
    release
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   751
  }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   752
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   753
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   754
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   755
  /** command line entry point **/
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   756
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   757
  def main(args: Array[String])
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   758
  {
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   759
    Command_Line.tool0 {
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   760
      var afp_rev = ""
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69432
diff changeset
   761
      var components_base: Path = Components.default_components_base
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   762
      var official_release = false
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   763
      var proper_release_name: Option[String] = None
64211
1306a0e7fe81 explicit website directory;
wenzelm
parents: 64210
diff changeset
   764
      var website: Option[Path] = None
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   765
      var build_sessions: List[String] = Nil
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   766
      var more_components: List[Path] = Nil
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   767
      var parallel_jobs = 1
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   768
      var build_library = false
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   769
      var options = Options.init()
64208
da9b04b8d204 clarified platform families vs. bundles;
wenzelm
parents: 64206
diff changeset
   770
      var platform_families = default_platform_families
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   771
      var rev = ""
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   772
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   773
      val getopts = Getopts("""
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   774
Usage: Admin/build_release [OPTIONS] BASE_DIR
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   775
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   776
  Options are:
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   777
    -A REV       corresponding AFP changeset id
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69432
diff changeset
   778
    -C DIR       base directory for Isabelle components (default: """ +
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69432
diff changeset
   779
        Components.default_components_base + """)
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   780
    -O           official release (not release-candidate)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   781
    -R RELEASE   proper release with name
64211
1306a0e7fe81 explicit website directory;
wenzelm
parents: 64210
diff changeset
   782
    -W WEBSITE   produce minimal website in given directory
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   783
    -b SESSIONS  build platform-specific session images (separated by commas)
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   784
    -c ARCHIVE   clean bundling with additional component .tar.gz archive
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   785
    -j INT       maximum number of parallel jobs (default 1)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   786
    -l           build library
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   787
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
65067
8bc9de2278c0 tuned message;
wenzelm
parents: 64936
diff changeset
   788
    -p NAMES     platform families (default: """ + default_platform_families.mkString(",") + """)
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   789
    -r REV       Mercurial changeset id (default: RELEASE or tip)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   790
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   791
  Build Isabelle release in base directory, using the local repository clone.
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   792
""",
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   793
        "A:" -> (arg => afp_rev = arg),
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69432
diff changeset
   794
        "C:" -> (arg => components_base = Path.explode(arg)),
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   795
        "O" -> (_ => official_release = true),
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   796
        "R:" -> (arg => proper_release_name = Some(arg)),
64211
1306a0e7fe81 explicit website directory;
wenzelm
parents: 64210
diff changeset
   797
        "W:" -> (arg => website = Some(Path.explode(arg))),
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   798
        "b:" -> (arg => build_sessions = space_explode(',', arg)),
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   799
        "c:" -> (arg =>
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   800
          {
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   801
            val path = Path.explode(arg)
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   802
            Components.Archive.get_name(path.file_name)
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   803
            more_components = more_components ::: List(path)
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   804
          }),
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   805
        "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   806
        "l" -> (_ => build_library = true),
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   807
        "o:" -> (arg => options = options + arg),
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   808
        "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)),
64204
db9ac35cae0d added option -p for platform families;
wenzelm
parents: 64203
diff changeset
   809
        "r:" -> (arg => rev = arg))
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   810
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   811
      val more_args = getopts(args)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   812
      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
   813
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   814
      val progress = new Console_Progress()
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   815
69415
99c3529c31d0 clarified error;
wenzelm
parents: 69414
diff changeset
   816
      if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
99c3529c31d0 clarified error;
wenzelm
parents: 69414
diff changeset
   817
        error("Building for windows requires 7z")
99c3529c31d0 clarified error;
wenzelm
parents: 69414
diff changeset
   818
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   819
      build_release(Path.explode(base_dir), options, components_base = components_base,
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   820
        progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release,
69397
df7d7477284b clarified signature;
wenzelm
parents: 69396
diff changeset
   821
        proper_release_name = proper_release_name, website = website,
64204
db9ac35cae0d added option -p for platform families;
wenzelm
parents: 64203
diff changeset
   822
        platform_families =
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   823
          if (platform_families.isEmpty) default_platform_families
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   824
          else platform_families,
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   825
        more_components = more_components, build_sessions = build_sessions,
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   826
        build_library = build_library, parallel_jobs = parallel_jobs)
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   827
    }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   828
  }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   829
}