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