src/Pure/Admin/build_release.scala
author wenzelm
Wed, 05 May 2021 14:07:25 +0200
changeset 73629 a771807df752
parent 73626 0732f66ce514
child 73630 f2e836e013cb
permissions -rw-r--r--
support for existing release archive; 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
{
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    12
  /** release context **/
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    13
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
    14
  private def execute(dir: Path, script: String): Unit =
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
    15
    Isabelle_System.bash(script, cwd = dir.file).check
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
    16
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
    17
  private def execute_tar(dir: Path, args: String, strip: Int = 0): Unit =
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
    18
    Isabelle_System.gnutar(args, dir = dir, strip = strip).check
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
    19
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    20
  object Release_Context
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    21
  {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    22
    def apply(
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    23
      target_dir: Path,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    24
      release_name: String = "",
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    25
      components_base: Path = Components.default_components_base,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    26
      progress: Progress = new Progress): Release_Context =
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    27
    {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    28
      val date = Date.now()
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    29
      val dist_name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date))
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    30
      val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    31
      new Release_Context(release_name, dist_name, dist_dir, components_base, progress)
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    32
    }
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    33
  }
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    34
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    35
  class Release_Context private[Build_Release](
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    36
    val release_name: String,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    37
    val dist_name: String,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    38
    val dist_dir: Path,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    39
    val components_base: Path,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    40
    val progress: Progress)
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    41
  {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    42
    override def toString: String = dist_name
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    43
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    44
    val isabelle: Path = Path.explode(dist_name)
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    45
    val isabelle_dir: Path = dist_dir + isabelle
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
    46
    val isabelle_archive: Path = dist_dir + isabelle.tar.gz
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    47
    val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    48
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    49
    def other_isabelle(dir: Path): Other_Isabelle =
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    50
      Other_Isabelle(dir + isabelle,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    51
        isabelle_identifier = dist_name + "-build",
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    52
        progress = progress)
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    53
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    54
    def make_announce(id: String): Unit =
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    55
    {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    56
      if (release_name.isEmpty) {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    57
        File.write(isabelle_dir + Path.explode("ANNOUNCE"),
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    58
          """
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    59
IMPORTANT NOTE
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    60
==============
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    61
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    62
This is a snapshot of Isabelle/""" + id + """ from the repository.
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    63
""")
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    64
      }
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    65
    }
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    66
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    67
    def make_contrib(): Unit =
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    68
    {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    69
      Isabelle_System.make_directory(Components.contrib(isabelle_dir))
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    70
      File.write(Components.contrib(isabelle_dir, name = "README"),
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    71
        """This directory contains add-on components that contribute to the main
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    72
Isabelle distribution.  Separate licensing conditions apply, see each
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    73
directory individually.
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    74
""")
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    75
    }
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    76
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    77
    def bundle_info(platform: Platform.Family.Value): Bundle_Info =
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    78
      platform match {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    79
        case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    80
        case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    81
        case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    82
      }
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    83
  }
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    84
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    85
  sealed case class Bundle_Info(
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
    86
    platform: Platform.Family.Value,
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    87
    platform_description: String,
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
    88
    name: String)
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    89
  {
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
    90
    def path: Path = Path.explode(name)
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    91
  }
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
    92
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    93
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    94
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    95
  /** release archive **/
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    96
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
    97
  val ISABELLE: Path = Path.basic("Isabelle")
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    98
  val ISABELLE_ID: Path = Path.explode("etc/ISABELLE_ID")
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
    99
  val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS")
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   100
  val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER")
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   101
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   102
  object Release_Archive
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   103
  {
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   104
    def make(bytes: Bytes, rename: String = ""): Release_Archive =
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   105
    {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   106
      Isabelle_System.with_tmp_dir("tmp")(dir =>
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   107
        Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   108
        {
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   109
          val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   110
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   111
          Bytes.write(archive_path, bytes)
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   112
          execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   113
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   114
          val id = File.read(isabelle_dir + ISABELLE_ID)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   115
          val tags = File.read(isabelle_dir + ISABELLE_TAGS)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   116
          val identifier = File.read(isabelle_dir + ISABELLE_IDENTIFIER)
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   117
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   118
          val (bytes1, identifier1) =
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   119
            if (rename.isEmpty || rename == identifier) (bytes, identifier)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   120
            else {
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   121
              File.write(isabelle_dir + ISABELLE_IDENTIFIER, rename)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   122
              Isabelle_System.move_file(isabelle_dir, dir + Path.basic(rename))
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   123
              execute_tar(dir, "-czf " + File.bash_path(archive_path) + " " + Bash.string(rename))
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   124
              (Bytes.read(archive_path), rename)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   125
            }
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   126
          new Release_Archive(bytes1, id, tags, identifier1)
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   127
        })
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   128
      )
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   129
    }
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   130
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   131
    def read(path: Path, rename: String = ""): Release_Archive =
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   132
      make(Bytes.read(path), rename = rename)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   133
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   134
    def get(url: String, rename: String = "", progress: Progress = new Progress): Release_Archive =
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   135
    {
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   136
      val bytes =
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   137
        if (Path.is_wellformed(url)) Bytes.read(Path.explode(url))
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   138
        else Isabelle_System.download(url, progress = progress).bytes
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   139
      make(bytes, rename = rename)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   140
    }
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   141
  }
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   142
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   143
  case class Release_Archive private[Build_Release](
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   144
    bytes: Bytes, id: String, tags: String, identifier: String)
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   145
  {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   146
    override def toString: String = identifier
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   147
  }
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   148
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   149
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   150
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   151
  /** generated content **/
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   152
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   153
  /* bundled components */
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   154
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   155
  class Bundled(platform: Option[Platform.Family.Value] = None)
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   156
  {
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   157
    def detect(s: String): Boolean =
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   158
      s.startsWith("#bundled") && !s.startsWith("#bundled ")
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   159
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   160
    def apply(name: String): String =
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   161
      "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   162
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   163
    private val Pattern1 = ("""^#bundled:(.*)$""").r
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   164
    private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   165
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   166
    def unapply(s: String): Option[String] =
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   167
      s match {
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   168
        case Pattern1(name) => Some(name)
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   169
        case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name)
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   170
        case _ => None
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   171
      }
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   172
  }
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   173
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73317
diff changeset
   174
  def record_bundled_components(dir: Path): Unit =
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   175
  {
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   176
    val catalogs =
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   177
      List("main", "bundled").map((_, new Bundled())) :::
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   178
      default_platform_families.flatMap(platform =>
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   179
        List(platform.toString, "bundled-" + platform.toString).
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   180
          map((_, new Bundled(platform = Some(platform)))))
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   181
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   182
    File.append(Components.components(dir),
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   183
      terminate_lines("#bundled components" ::
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   184
        (for {
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   185
          (catalog, bundled) <- catalogs.iterator
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71542
diff changeset
   186
          path = Components.admin(dir) + Path.basic(catalog)
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   187
          if path.is_file
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   188
          line <- split_lines(File.read(path))
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   189
          if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   190
        } yield bundled(line)).toList))
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   191
  }
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   192
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   193
  def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) =
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   194
  {
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   195
    val Bundled = new Bundled(platform = Some(platform))
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   196
    val components =
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   197
      for {
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   198
        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
   199
        if !name.startsWith("jedit_build")
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   200
      } yield name
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   201
    val jdk_component =
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   202
      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
   203
    (components, jdk_component)
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   204
  }
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   205
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73317
diff changeset
   206
  def activate_components(
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73317
diff changeset
   207
    dir: Path, platform: Platform.Family.Value, more_names: List[String]): Unit =
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   208
  {
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   209
    def contrib_name(name: String): String =
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   210
      Components.contrib(name = name).implode
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   211
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   212
    val Bundled = new Bundled(platform = Some(platform))
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   213
    Components.write_components(dir,
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   214
      Components.read_components(dir).flatMap(line =>
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   215
        line match {
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   216
          case Bundled(name) =>
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   217
            if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   218
            else None
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents: 69392
diff changeset
   219
          case _ => if (Bundled.detect(line)) None else Some(line)
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71542
diff changeset
   220
        }) ::: more_names.map(contrib_name))
69391
a3c776b9d3dd manage components similar to makedist_bundle (still inactive);
wenzelm
parents: 69390
diff changeset
   221
  }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   222
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   223
70099
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   224
  /** build release **/
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   225
70099
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   226
  /* build heaps on remote server */
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   227
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   228
  private def remote_build_heaps(
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   229
    options: Options,
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   230
    platform: Platform.Family.Value,
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   231
    build_sessions: List[String],
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73317
diff changeset
   232
    local_dir: Path): Unit =
70099
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   233
  {
72341
0973a594be72 clarified names;
wenzelm
parents: 71973
diff changeset
   234
    val server_option = "build_host_" + platform.toString
70099
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   235
    options.string(server_option) match {
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   236
      case SSH.Target(user, host) =>
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   237
        using(SSH.open_session(options, host = host, user = user))(ssh =>
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   238
          Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar =>
70099
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   239
          {
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   240
            execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   241
            ssh.with_tmp_dir(remote_dir =>
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   242
            {
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   243
              val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   244
              ssh.write_file(remote_tmp_tar, local_tmp_tar)
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   245
              val remote_commands =
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   246
                List(
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   247
                  "cd " + File.bash_path(remote_dir),
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   248
                  "tar -xf tmp.tar",
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   249
                  "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
70099
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   250
                  "tar -cf tmp.tar heaps")
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   251
              ssh.execute(remote_commands.mkString(" && ")).check
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   252
              ssh.read_file(remote_tmp_tar, local_tmp_tar)
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   253
            })
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   254
            execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   255
          })
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   256
        )
70099
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   257
      case s => error("Bad " + server_option + ": " + quote(s))
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   258
    }
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   259
  }
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   260
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   261
73066
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   262
  /* Isabelle application */
73060
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   263
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73317
diff changeset
   264
  def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n"): Unit =
73068
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   265
  {
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   266
    val title = "# Java runtime options"
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   267
    File.write(path, (title :: options).map(_ + line_ending).mkString)
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   268
  }
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   269
73065
dd68f20d4041 tuned signature;
wenzelm
parents: 73064
diff changeset
   270
  def make_isabelle_app(
73193
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   271
    platform: Platform.Family.Value,
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   272
    isabelle_target: Path,
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   273
    isabelle_name: String,
73065
dd68f20d4041 tuned signature;
wenzelm
parents: 73064
diff changeset
   274
    jdk_component: String,
73095
d08cbc36a99a clarified dock icon: setup earlier on startup;
wenzelm
parents: 73085
diff changeset
   275
    classpath: List[Path],
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73317
diff changeset
   276
    dock_icon: Boolean = false): Unit =
73064
21af3a90d194 tuned signature;
wenzelm
parents: 73063
diff changeset
   277
  {
21af3a90d194 tuned signature;
wenzelm
parents: 73063
diff changeset
   278
    val script = """#!/usr/bin/env bash
73060
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   279
#
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   280
# Author: Makarius
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   281
#
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   282
# Main Isabelle application script.
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   283
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   284
# minimal Isabelle environment
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   285
73193
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   286
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)"
73060
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   287
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   288
73063
f0180048d5ff updated according to ~~/etc/settings;
wenzelm
parents: 73062
diff changeset
   289
#paranoia settings -- avoid intrusion of alien options
f0180048d5ff updated according to ~~/etc/settings;
wenzelm
parents: 73062
diff changeset
   290
unset "_JAVA_OPTIONS"
f0180048d5ff updated according to ~~/etc/settings;
wenzelm
parents: 73062
diff changeset
   291
unset "JAVA_TOOL_OPTIONS"
f0180048d5ff updated according to ~~/etc/settings;
wenzelm
parents: 73062
diff changeset
   292
f0180048d5ff updated according to ~~/etc/settings;
wenzelm
parents: 73062
diff changeset
   293
#paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc.
f0180048d5ff updated according to ~~/etc/settings;
wenzelm
parents: 73062
diff changeset
   294
unset XMODIFIERS
f0180048d5ff updated according to ~~/etc/settings;
wenzelm
parents: 73062
diff changeset
   295
73062
0b0c651e823f more portable component setup;
wenzelm
parents: 73061
diff changeset
   296
COMPONENT="$ISABELLE_HOME/contrib/""" + jdk_component + """"
0b0c651e823f more portable component setup;
wenzelm
parents: 73061
diff changeset
   297
source "$COMPONENT/etc/settings"
0b0c651e823f more portable component setup;
wenzelm
parents: 73061
diff changeset
   298
73060
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   299
73063
f0180048d5ff updated according to ~~/etc/settings;
wenzelm
parents: 73062
diff changeset
   300
# main
73060
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   301
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   302
declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options"))
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   303
73197
d967f6643f5e proper Isabelle environment (amending 31fbde3baa97);
wenzelm
parents: 73193
diff changeset
   304
"$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup"
73153
96d87b9c2b42 workaround for Big Sur fullscreen mode: better support for JDialog windows (e.g. Find on top of main View);
wenzelm
parents: 73152
diff changeset
   305
73062
0b0c651e823f more portable component setup;
wenzelm
parents: 73061
diff changeset
   306
exec "$ISABELLE_JDK_HOME/bin/java" \
73060
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   307
  "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
73061
abaff6fb0ff2 clarified quotes;
wenzelm
parents: 73060
diff changeset
   308
  -classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \
73060
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   309
  "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
73095
d08cbc36a99a clarified dock icon: setup earlier on startup;
wenzelm
parents: 73085
diff changeset
   310
""" + (if (dock_icon) """"-Xdock:icon=$ISABELLE_HOME/lib/logo/isabelle_transparent-128.png" \
d08cbc36a99a clarified dock icon: setup earlier on startup;
wenzelm
parents: 73085
diff changeset
   311
""" else "") + """isabelle.Main "$@"
73060
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   312
"""
73193
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   313
    val script_path = isabelle_target + Path.explode("lib/scripts/Isabelle_app")
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   314
    File.write(script_path, script)
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   315
    File.set_executable(script_path, true)
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   316
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   317
    val component_dir = isabelle_target + Path.explode("contrib/Isabelle_app")
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73197
diff changeset
   318
    Isabelle_System.move_file(
73193
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   319
      component_dir + Path.explode(Platform.standard_platform(platform)) + Path.explode("Isabelle"),
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   320
      isabelle_target + Path.explode(isabelle_name))
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   321
    Isabelle_System.rm_tree(component_dir)
73064
21af3a90d194 tuned signature;
wenzelm
parents: 73063
diff changeset
   322
  }
73060
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   323
4b620e1cb1e9 tuned -- generate script by Isabelle/Scala;
wenzelm
parents: 72387
diff changeset
   324
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73317
diff changeset
   325
  def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String): Unit =
73066
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   326
  {
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   327
    File.write(path, """<?xml version="1.0" ?>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   328
<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   329
<plist version="1.0">
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   330
<dict>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   331
<key>CFBundleDevelopmentRegion</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   332
<string>English</string>
73075
893310d6d76d recovered bundle icons (not application) from macos_app;
wenzelm
parents: 73074
diff changeset
   333
<key>CFBundleIconFile</key>
893310d6d76d recovered bundle icons (not application) from macos_app;
wenzelm
parents: 73074
diff changeset
   334
<string>isabelle.icns</string>
73066
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   335
<key>CFBundleIdentifier</key>
73152
5a954fd5f078 clarified app identification, potentially relevant for macOS "defaults";
wenzelm
parents: 73112
diff changeset
   336
<string>de.tum.in.isabelle</string>
73066
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   337
<key>CFBundleDisplayName</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   338
<string>""" + isabelle_name + """</string>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   339
<key>CFBundleInfoDictionaryVersion</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   340
<string>6.0</string>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   341
<key>CFBundleName</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   342
<string>""" + isabelle_name + """</string>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   343
<key>CFBundlePackageType</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   344
<string>APPL</string>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   345
<key>CFBundleShortVersionString</key>
73152
5a954fd5f078 clarified app identification, potentially relevant for macOS "defaults";
wenzelm
parents: 73112
diff changeset
   346
<string>""" + isabelle_name + """</string>
73066
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   347
<key>CFBundleSignature</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   348
<string>????</string>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   349
<key>CFBundleVersion</key>
73152
5a954fd5f078 clarified app identification, potentially relevant for macOS "defaults";
wenzelm
parents: 73112
diff changeset
   350
<string>""" + isabelle_rev + """</string>
73066
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   351
<key>NSHumanReadableCopyright</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   352
<string></string>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   353
<key>LSMinimumSystemVersion</key>
73085
b595bcdf5bf3 proper LSMinimumSystemVersion for zulu-jdk-15;
wenzelm
parents: 73083
diff changeset
   354
<string>10.11</string>
73066
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   355
<key>LSApplicationCategoryType</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   356
<string>public.app-category.developer-tools</string>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   357
<key>NSHighResolutionCapable</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   358
<string>true</string>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   359
<key>NSSupportsAutomaticGraphicsSwitching</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   360
<string>true</string>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   361
<key>CFBundleDocumentTypes</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   362
<array>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   363
<dict>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   364
<key>CFBundleTypeExtensions</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   365
<array>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   366
<string>thy</string>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   367
</array>
73077
75bd49ba9c28 recovered file-type icons from macos_app;
wenzelm
parents: 73075
diff changeset
   368
<key>CFBundleTypeIconFile</key>
75bd49ba9c28 recovered file-type icons from macos_app;
wenzelm
parents: 73075
diff changeset
   369
<string>theory.icns</string>
73066
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   370
<key>CFBundleTypeName</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   371
<string>Isabelle theory file</string>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   372
<key>CFBundleTypeRole</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   373
<string>Editor</string>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   374
<key>LSTypeIsPackage</key>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   375
<false/>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   376
</dict>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   377
</array>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   378
</dict>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   379
</plist>
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   380
""")
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   381
  }
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   382
27f79e7eb356 tuned -- generate Info.plist in Isabelle/Scala;
wenzelm
parents: 73065
diff changeset
   383
73064
21af3a90d194 tuned signature;
wenzelm
parents: 73063
diff changeset
   384
  /* main */
70099
9b9c1192f972 support for platform-specific builds on remote server;
wenzelm
parents: 70098
diff changeset
   385
69415
99c3529c31d0 clarified error;
wenzelm
parents: 69414
diff changeset
   386
  private val default_platform_families: List[Platform.Family.Value] =
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   387
    List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
64204
db9ac35cae0d added option -p for platform families;
wenzelm
parents: 64203
diff changeset
   388
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   389
  def use_release_archive(
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   390
    context: Release_Context,
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   391
    archive: Release_Archive,
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   392
    id: String = ""): Unit =
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   393
  {
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   394
    if (id.nonEmpty && id != archive.id) {
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   395
      error("Mismatch of release identification " + id + " vs. archive " + archive.id)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   396
    }
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   397
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   398
    if (!context.isabelle_archive.is_file || Bytes.read(context.isabelle_archive) != archive.bytes) {
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   399
      Bytes.write(context.isabelle_archive, archive.bytes)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   400
    }
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   401
  }
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   402
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   403
  def build_release_archive(
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   404
    context: Release_Context,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   405
    version: String,
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   406
    parallel_jobs: Int = 1): Unit =
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   407
  {
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   408
    val progress = context.progress
69174
822726043e28 misc tuning and clarification;
wenzelm
parents: 69171
diff changeset
   409
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   410
    val hg = Mercurial.repository(Path.ISABELLE_HOME)
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   411
    val id =
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   412
      try { hg.id(version) }
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   413
      catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   414
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   415
    if (context.isabelle_archive.is_file) {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   416
      progress.echo_warning("Found existing release archive: " + context.isabelle_archive)
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   417
      use_release_archive(context, Release_Archive.read(context.isabelle_archive), id = id)
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   418
    }
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   419
    else {
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   420
      progress.echo_warning("Preparing release " + context.dist_name + " ...")
64221
407f69c4959f identify release;
wenzelm
parents: 64212
diff changeset
   421
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   422
      Isabelle_System.new_directory(context.dist_dir)
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   423
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   424
      hg.archive(context.isabelle_dir.expand.implode, rev = id, options = "--type files")
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   425
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   426
      for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   427
        (context.isabelle_dir + Path.explode(name)).file.delete
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   428
      }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   429
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   430
      File.write(context.isabelle_dir + ISABELLE_ID, id)
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   431
      File.write(context.isabelle_dir + ISABELLE_TAGS, hg.tags(rev = id))
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   432
      File.write(context.isabelle_dir + ISABELLE_IDENTIFIER, context.dist_name)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   433
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   434
      context.make_announce(id)
73520
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73519
diff changeset
   435
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   436
      context.make_contrib()
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   437
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   438
      execute(context.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
   439
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   440
      record_bundled_components(context.isabelle_dir)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   441
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   442
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   443
      /* build tools and documentation */
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   444
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   445
      val other_isabelle = context.other_isabelle(context.dist_dir)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   446
69388
fc58534bc475 clarified component settings;
wenzelm
parents: 69387
diff changeset
   447
      other_isabelle.init_settings(
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   448
        other_isabelle.init_components(
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   449
          components_base = context.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
   450
      other_isabelle.resolve_components(echo = true)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   451
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   452
      try {
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   453
        val export_classpath =
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   454
          "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   455
        other_isabelle.bash(export_classpath + "Admin/build all", echo = true).check
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   456
        other_isabelle.bash(export_classpath + "bin/isabelle jedit -b", echo = true).check
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   457
      }
71936
12f455cc6573 clarified errors;
wenzelm
parents: 71932
diff changeset
   458
      catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   459
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   460
      try {
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   461
        other_isabelle.bash(
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   462
          "bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   463
      }
71936
12f455cc6573 clarified errors;
wenzelm
parents: 71932
diff changeset
   464
      catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   465
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   466
      other_isabelle.make_news()
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   467
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   468
      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
   469
        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
   470
      }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   471
69171
710845a85944 more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents: 69170
diff changeset
   472
      other_isabelle.cleanup()
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   473
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   474
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   475
      progress.echo_warning("Creating release archive " + context.isabelle_archive + " ...")
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   476
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   477
      execute(context.dist_dir, """chmod -R a+r . && chmod -R u+w . && chmod -R g=o .""")
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   478
      execute(context.dist_dir,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   479
        """find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""")
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   480
      execute_tar(context.dist_dir, "-czf " +
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   481
        File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name))
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   482
    }
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   483
  }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   484
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   485
  def build_release(
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   486
    options: Options,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   487
    context: Release_Context,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   488
    afp_rev: String = "",
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   489
    platform_families: List[Platform.Family.Value] = default_platform_families,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   490
    more_components: List[Path] = Nil,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   491
    website: Option[Path] = None,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   492
    build_sessions: List[String] = Nil,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   493
    build_library: Boolean = false,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   494
    parallel_jobs: Int = 1): Unit =
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   495
  {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   496
    val progress = context.progress
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   497
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   498
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   499
    /* release directory */
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   500
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   501
    val archive = Release_Archive.read(context.isabelle_archive)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   502
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   503
    for (path <- List(context.isabelle, ISABELLE)) {
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   504
      Isabelle_System.rm_tree(context.dist_dir + path)
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   505
    }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   506
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   507
    Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   508
    {
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   509
      Bytes.write(archive_path, archive.bytes)
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   510
      val extract =
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   511
        List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc").
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   512
          map(name => context.release_name + "/" + name)
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   513
      execute_tar(context.dist_dir,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   514
        "-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract))
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   515
    })
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   516
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   517
    Isabelle_System.symlink(Path.explode(context.dist_name), context.dist_dir + ISABELLE)
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   518
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   519
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   520
    /* make application bundles */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   521
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   522
    val bundle_infos = platform_families.map(context.bundle_info)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   523
66730
wenzelm
parents: 66724
diff changeset
   524
    for (bundle_info <- bundle_infos) {
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   525
      val isabelle_name = context.dist_name
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   526
      val platform = bundle_info.platform
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   527
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   528
      progress.echo("\nApplication bundle for " + platform)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   529
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   530
      Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   531
      {
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   532
        // release archive
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   533
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   534
        execute_tar(tmp_dir, "-xzf " + File.bash_path(context.isabelle_archive))
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   535
        val other_isabelle = context.other_isabelle(tmp_dir)
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   536
        val isabelle_target = other_isabelle.isabelle_home
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   537
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   538
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   539
        // bundled components
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   540
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   541
        progress.echo("Bundled components:")
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   542
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   543
        val contrib_dir = Components.contrib(isabelle_target)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   544
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   545
        val (bundled_components, jdk_component) =
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   546
          get_bundled_components(isabelle_target, platform)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   547
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   548
        Components.resolve(context.components_base, bundled_components,
70102
e48ffba6b557 retain copy of required components;
wenzelm
parents: 70101
diff changeset
   549
          target_dir = Some(contrib_dir),
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   550
          copy_dir = Some(context.dist_dir + Path.explode("contrib")),
70102
e48ffba6b557 retain copy of required components;
wenzelm
parents: 70101
diff changeset
   551
          progress = progress)
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   552
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   553
        val more_components_names =
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   554
          more_components.map(Components.unpack(contrib_dir, _, progress = progress))
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   555
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   556
        Components.purge(contrib_dir, platform)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   557
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   558
        activate_components(isabelle_target, platform, more_components_names)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   559
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   560
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   561
        // Java parameters
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   562
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   563
        val java_options: List[String] =
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   564
          (for {
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   565
            variable <-
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   566
              List(
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   567
                "ISABELLE_JAVA_SYSTEM_OPTIONS",
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   568
                "JEDIT_JAVA_SYSTEM_OPTIONS",
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   569
                "JEDIT_JAVA_OPTIONS")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   570
            opt <- Word.explode(other_isabelle.getenv(variable))
73068
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   571
          }
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   572
          yield {
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   573
            val s = "-Dapple.awt.application.name="
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   574
            if (opt.startsWith(s)) s + isabelle_name else opt
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   575
          }) ::: List("-Disabelle.jedit_server=" + isabelle_name)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   576
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   577
        val classpath: List[Path] =
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   578
        {
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   579
          val base = isabelle_target.absolute
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   580
          Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   581
          {
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   582
            val abs_path = path.absolute
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   583
            File.relative_path(base, abs_path) match {
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   584
              case Some(rel_path) => rel_path
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   585
              case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   586
            }
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   587
          }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   588
        }
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   589
71542
e76692ec6e5a more usable defaults for high resolution on Linux, where the desktop environment usually lacks automatic scaling;
wenzelm
parents: 71459
diff changeset
   590
        val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   591
        val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   592
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   593
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   594
        // build heaps
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   595
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   596
        if (build_sessions.nonEmpty) {
70103
a6236d5a89ae tuned message;
wenzelm
parents: 70102
diff changeset
   597
          progress.echo("Building heaps ...")
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   598
          remote_build_heaps(options, platform, build_sessions, isabelle_target)
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   599
        }
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   600
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   601
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   602
        // application bundling
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   603
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   604
        platform match {
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   605
          case Platform.Family.linux =>
72378
075f3cbc7546 clarified signature;
wenzelm
parents: 72376
diff changeset
   606
            File.change(isabelle_target + jedit_options,
075f3cbc7546 clarified signature;
wenzelm
parents: 72376
diff changeset
   607
              _.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24"))
71542
e76692ec6e5a more usable defaults for high resolution on Linux, where the desktop environment usually lacks automatic scaling;
wenzelm
parents: 71459
diff changeset
   608
72378
075f3cbc7546 clarified signature;
wenzelm
parents: 72376
diff changeset
   609
            File.change(isabelle_target + jedit_props,
075f3cbc7546 clarified signature;
wenzelm
parents: 72376
diff changeset
   610
              _.replaceAll("console.fontsize=.*", "console.fontsize=18")
075f3cbc7546 clarified signature;
wenzelm
parents: 72376
diff changeset
   611
               .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18")
075f3cbc7546 clarified signature;
wenzelm
parents: 72376
diff changeset
   612
               .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18")
075f3cbc7546 clarified signature;
wenzelm
parents: 72376
diff changeset
   613
               .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18")
075f3cbc7546 clarified signature;
wenzelm
parents: 72376
diff changeset
   614
               .replaceAll("view.fontsize=.*", "view.fontsize=24")
075f3cbc7546 clarified signature;
wenzelm
parents: 72376
diff changeset
   615
               .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16"))
71542
e76692ec6e5a more usable defaults for high resolution on Linux, where the desktop environment usually lacks automatic scaling;
wenzelm
parents: 71459
diff changeset
   616
73068
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   617
            make_isabelle_options(
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   618
              isabelle_target + Path.explode("Isabelle.options"), java_options)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   619
73193
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   620
            make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath)
69417
wenzelm
parents: 69415
diff changeset
   621
70246
7c55ea37fbf7 back to gz for linux (and macos) -- xz is too slow and cumbersome;
wenzelm
parents: 70244
diff changeset
   622
            val archive_name = isabelle_name + "_linux.tar.gz"
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   623
            progress.echo("Packaging " + archive_name + " ...")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   624
            execute_tar(tmp_dir,
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   625
              "-czf " + File.bash_path(context.dist_dir + Path.explode(archive_name)) + " " +
70242
wenzelm
parents: 70207
diff changeset
   626
              Bash.string(isabelle_name))
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   627
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
   628
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   629
          case Platform.Family.macos =>
72378
075f3cbc7546 clarified signature;
wenzelm
parents: 72376
diff changeset
   630
            File.change(isabelle_target + jedit_props,
73112
efc58b56a6c7 clarified default L&F;
wenzelm
parents: 73095
diff changeset
   631
              _.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
72378
075f3cbc7546 clarified signature;
wenzelm
parents: 72376
diff changeset
   632
               .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
69417
wenzelm
parents: 69415
diff changeset
   633
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   634
73193
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   635
            // macOS application bundle
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   636
73193
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   637
            val app_contents = isabelle_target + Path.explode("Contents")
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   638
73077
75bd49ba9c28 recovered file-type icons from macos_app;
wenzelm
parents: 73075
diff changeset
   639
            for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) {
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73197
diff changeset
   640
              Isabelle_System.copy_file(isabelle_target + Path.explode(icon),
73193
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   641
                Isabelle_System.make_directory(app_contents + Path.explode("Resources")))
73077
75bd49ba9c28 recovered file-type icons from macos_app;
wenzelm
parents: 73075
diff changeset
   642
            }
73075
893310d6d76d recovered bundle icons (not application) from macos_app;
wenzelm
parents: 73074
diff changeset
   643
73083
4a117b57e622 clarified Info.plist;
wenzelm
parents: 73077
diff changeset
   644
            make_isabelle_plist(
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   645
              app_contents + Path.explode("Info.plist"), isabelle_name, archive.id)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   646
73193
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   647
            make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component,
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   648
              classpath, dock_icon = true)
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   649
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   650
            val isabelle_options = Path.explode("Isabelle.options")
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   651
            make_isabelle_options(
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   652
              isabelle_target + isabelle_options,
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   653
              java_options ::: List("-Disabelle.app=true"))
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   654
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   655
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   656
            // application archive
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   657
70244
2ca87b481077 back to gz for macos: more robust;
wenzelm
parents: 70243
diff changeset
   658
            val archive_name = isabelle_name + "_macos.tar.gz"
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   659
            progress.echo("Packaging " + archive_name + " ...")
73193
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   660
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   661
            val isabelle_app = Path.explode(isabelle_name + ".app")
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73197
diff changeset
   662
            Isabelle_System.move_file(tmp_dir + Path.explode(isabelle_name),
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73197
diff changeset
   663
              tmp_dir + isabelle_app)
73193
b8e12e94cfca more uniform directory layout for macOS;
wenzelm
parents: 73161
diff changeset
   664
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   665
            execute_tar(tmp_dir,
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   666
              "-czf " + File.bash_path(context.dist_dir + Path.explode(archive_name)) + " " +
70242
wenzelm
parents: 70207
diff changeset
   667
              File.bash_path(isabelle_app))
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
   668
69417
wenzelm
parents: 69415
diff changeset
   669
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   670
          case Platform.Family.windows =>
72378
075f3cbc7546 clarified signature;
wenzelm
parents: 72376
diff changeset
   671
            File.change(isabelle_target + jedit_props,
73112
efc58b56a6c7 clarified default L&F;
wenzelm
parents: 73095
diff changeset
   672
              _.replaceAll("foldPainter=.*", "foldPainter=Square"))
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   673
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   674
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   675
            // application launcher
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   676
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73197
diff changeset
   677
            Isabelle_System.move_file(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   678
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   679
            val app_template = Path.explode("~~/Admin/Windows/launch4j")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   680
73068
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   681
            make_isabelle_options(
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   682
              isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
a95f5ae5a12a discontinued macOS JavaAppLauncher: re-use plain shell script;
wenzelm
parents: 73067
diff changeset
   683
              java_options, line_ending = "\r\n")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   684
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   685
            val isabelle_xml = Path.explode("isabelle.xml")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   686
            val isabelle_exe = Path.explode(isabelle_name + ".exe")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   687
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   688
            File.write(tmp_dir + isabelle_xml,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   689
              File.read(app_template + isabelle_xml)
72387
wenzelm
parents: 72378
diff changeset
   690
                .replace("{ISABELLE_NAME}", isabelle_name)
wenzelm
parents: 72378
diff changeset
   691
                .replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe))
wenzelm
parents: 72378
diff changeset
   692
                .replace("{ICON}",
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   693
                  File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
72387
wenzelm
parents: 72378
diff changeset
   694
                .replace("{SPLASH}",
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   695
                  File.platform_path(app_template + Path.explode("isabelle.bmp")))
72387
wenzelm
parents: 72378
diff changeset
   696
                .replace("{CLASSPATH}",
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   697
                  cat_lines(classpath.map(cp =>
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   698
                    "    <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>")))
72387
wenzelm
parents: 72378
diff changeset
   699
                .replace("\\jdk\\", "\\" + jdk_component + "\\"))
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   700
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   701
            execute(tmp_dir,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   702
              "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   703
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73197
diff changeset
   704
            Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"),
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   705
              isabelle_target + isabelle_exe.ext("manifest"))
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   706
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   707
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   708
            // Cygwin setup
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   709
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   710
            val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   711
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73197
diff changeset
   712
            Isabelle_System.copy_file(cygwin_template + Path.explode("Cygwin-Terminal.bat"),
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73197
diff changeset
   713
              isabelle_target)
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   714
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   715
            val cygwin_mirror =
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   716
              File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   717
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   718
            val cygwin_bat = Path.explode("Cygwin-Setup.bat")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   719
            File.write(isabelle_target + cygwin_bat,
72387
wenzelm
parents: 72378
diff changeset
   720
              File.read(cygwin_template + cygwin_bat).replace("{MIRROR}", cygwin_mirror))
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   721
            File.set_executable(isabelle_target + cygwin_bat, true)
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   722
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   723
            for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   724
              val path = Path.explode(name)
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73197
diff changeset
   725
              Isabelle_System.copy_file(cygwin_template + path,
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   726
                isabelle_target + Path.explode("contrib/cygwin") + path)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   727
            }
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   728
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   729
            execute(isabelle_target,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   730
              """find . -type f -not -name "*.exe" -not -name "*.dll" """ +
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   731
              (if (Platform.is_macos) "-perm +100" else "-executable") +
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   732
              " -print0 > contrib/cygwin/isabelle/executables")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   733
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   734
            execute(isabelle_target,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   735
              """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   736
              """> contrib/cygwin/isabelle/symlinks""")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   737
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   738
            execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   739
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   740
            File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   741
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   742
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   743
            // executable archive (self-extracting 7z)
69424
840f0cadeba8 clarified application bundling: discontinued redundant archives;
wenzelm
parents: 69417
diff changeset
   744
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   745
            val archive_name = isabelle_name + ".7z"
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   746
            val exe_archive = tmp_dir + Path.explode(archive_name)
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   747
            exe_archive.file.delete
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   748
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   749
            progress.echo("Packaging " + archive_name + " ...")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   750
            execute(tmp_dir,
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   751
              "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   752
            if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   753
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   754
            val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   755
            val sfx_txt =
72387
wenzelm
parents: 72378
diff changeset
   756
              File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt"))
wenzelm
parents: 72378
diff changeset
   757
                .replace("{ISABELLE_NAME}", isabelle_name)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   758
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   759
            Bytes.write(context.dist_dir + isabelle_exe,
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   760
              Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   761
            File.set_executable(context.dist_dir + isabelle_exe, true)
70098
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   762
        }
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   763
      })
956d2430cb29 more robust: always (re)build platform application bundles;
wenzelm
parents: 70046
diff changeset
   764
      progress.echo("DONE")
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   765
    }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   766
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   767
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   768
    /* minimal website */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   769
64361
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   770
    for (dir <- website) {
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   771
      val website_platform_bundles =
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   772
        for {
66730
wenzelm
parents: 66724
diff changeset
   773
          bundle_info <- bundle_infos
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   774
          if (context.dist_dir + bundle_info.path).is_file
69432
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69425
diff changeset
   775
        } yield (bundle_info.name, bundle_info)
64206
cb98e0e5f1e5 website index for existing bundles;
wenzelm
parents: 64205
diff changeset
   776
71275
18f4061fd817 tuned index.html;
wenzelm
parents: 70246
diff changeset
   777
      val isabelle_link =
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   778
        HTML.link(Isabelle_System.isabelle_repository.changeset(archive.id),
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   779
          HTML.text("Isabelle/" + archive.id))
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   780
      val afp_link =
73610
6ba5f9d18c56 clarified signature: more operations;
wenzelm
parents: 73609
diff changeset
   781
        HTML.link(Isabelle_System.afp_repository.changeset(afp_rev),
6ba5f9d18c56 clarified signature: more operations;
wenzelm
parents: 73609
diff changeset
   782
          HTML.text("AFP/" + afp_rev))
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   783
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   784
      HTML.write_document(dir, "index.html",
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   785
        List(HTML.title(context.dist_name)),
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   786
        List(
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   787
          HTML.section(context.dist_name),
73626
0732f66ce514 more website content;
wenzelm
parents: 73625
diff changeset
   788
          HTML.subsection("Downloads"),
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   789
          HTML.itemize(
73626
0732f66ce514 more website content;
wenzelm
parents: 73625
diff changeset
   790
            List(HTML.link(context.dist_name + ".tar.gz", HTML.text("Source archive"))) ::
66730
wenzelm
parents: 66724
diff changeset
   791
            website_platform_bundles.map({ case (bundle, bundle_info) =>
73626
0732f66ce514 more website content;
wenzelm
parents: 73625
diff changeset
   792
              List(HTML.link(bundle, HTML.text(bundle_info.platform_description + " bundle"))) })),
71275
18f4061fd817 tuned index.html;
wenzelm
parents: 70246
diff changeset
   793
          HTML.subsection("Repositories"),
18f4061fd817 tuned index.html;
wenzelm
parents: 70246
diff changeset
   794
          HTML.itemize(
18f4061fd817 tuned index.html;
wenzelm
parents: 70246
diff changeset
   795
            List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   796
73626
0732f66ce514 more website content;
wenzelm
parents: 73625
diff changeset
   797
      Isabelle_System.copy_file(context.isabelle_archive, dir)
0732f66ce514 more website content;
wenzelm
parents: 73625
diff changeset
   798
0732f66ce514 more website content;
wenzelm
parents: 73625
diff changeset
   799
      for ((bundle, _) <- website_platform_bundles) {
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   800
        Isabelle_System.copy_file(context.dist_dir + Path.explode(bundle), dir)
73626
0732f66ce514 more website content;
wenzelm
parents: 73625
diff changeset
   801
      }
64361
07d910a58a14 misc tuning and clarification;
wenzelm
parents: 64360
diff changeset
   802
    }
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   803
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   804
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   805
    /* HTML library */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   806
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   807
    if (build_library) {
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   808
      if (context.isabelle_library_archive.is_file) {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   809
        progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive)
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   810
      }
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   811
      else {
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   812
        Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   813
          {
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   814
            val bundle =
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   815
              context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz")
70246
7c55ea37fbf7 back to gz for linux (and macos) -- xz is too slow and cumbersome;
wenzelm
parents: 70244
diff changeset
   816
            execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   817
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   818
            val other_isabelle = context.other_isabelle(tmp_dir)
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   819
72375
e48d93811ed7 clarified signature;
wenzelm
parents: 72341
diff changeset
   820
            Isabelle_System.make_directory(other_isabelle.etc)
68755
67d6f1708ea4 enforce ML_system_64: more robust as cold build, without command_timings;
wenzelm
parents: 67045
diff changeset
   821
            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
   822
70243
b134cf366c2c proper arguments for library build;
wenzelm
parents: 70242
diff changeset
   823
            other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
69406
wenzelm
parents: 69405
diff changeset
   824
              " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
69873
6ebe97815275 proper option (amending cc0b3e177b49);
wenzelm
parents: 69789
diff changeset
   825
              " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   826
            other_isabelle.isabelle_home_user.file.delete
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   827
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   828
            execute(tmp_dir, "chmod -R a+r " + Bash.string(context.dist_name))
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   829
            execute(tmp_dir, "chmod -R g=o " + Bash.string(context.dist_name))
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   830
            execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   831
              " " + Bash.string(context.dist_name + "/browser_info"))
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   832
          })
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   833
      }
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   834
    }
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   835
  }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   836
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   837
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   838
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   839
  /** command line entry point **/
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   840
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73317
diff changeset
   841
  def main(args: Array[String]): Unit =
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   842
  {
71632
c1bc38327bc2 clarified signature;
wenzelm
parents: 71601
diff changeset
   843
    Command_Line.tool {
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   844
      var afp_rev = ""
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69432
diff changeset
   845
      var components_base: Path = Components.default_components_base
73607
fc13738e1933 clarified command-line, following other build_XYZ tools;
wenzelm
parents: 73582
diff changeset
   846
      var target_dir = Path.current
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   847
      var release_name = ""
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   848
      var source_archive = ""
64211
1306a0e7fe81 explicit website directory;
wenzelm
parents: 64210
diff changeset
   849
      var website: Option[Path] = None
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   850
      var build_sessions: List[String] = Nil
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   851
      var more_components: List[Path] = Nil
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   852
      var parallel_jobs = 1
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   853
      var build_library = false
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   854
      var options = Options.init()
64208
da9b04b8d204 clarified platform families vs. bundles;
wenzelm
parents: 64206
diff changeset
   855
      var platform_families = default_platform_families
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   856
      var rev = ""
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   857
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   858
      val getopts = Getopts("""
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   859
Usage: Admin/build_release [OPTIONS] BASE_DIR
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   860
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   861
  Options are:
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   862
    -A REV       corresponding AFP changeset id
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69432
diff changeset
   863
    -C DIR       base directory for Isabelle components (default: """ +
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69432
diff changeset
   864
        Components.default_components_base + """)
73607
fc13738e1933 clarified command-line, following other build_XYZ tools;
wenzelm
parents: 73582
diff changeset
   865
    -D DIR       target directory (default ".")
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   866
    -R RELEASE   explicit release name
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   867
    -S ARCHIVE   use existing source archive (file or URL)
64211
1306a0e7fe81 explicit website directory;
wenzelm
parents: 64210
diff changeset
   868
    -W WEBSITE   produce minimal website in given directory
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   869
    -b SESSIONS  build platform-specific session images (separated by commas)
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   870
    -c ARCHIVE   clean bundling with additional component .tar.gz archive
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   871
    -j INT       maximum number of parallel jobs (default 1)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   872
    -l           build library
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   873
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
65067
8bc9de2278c0 tuned message;
wenzelm
parents: 64936
diff changeset
   874
    -p NAMES     platform families (default: """ + default_platform_families.mkString(",") + """)
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   875
    -r REV       Mercurial changeset id (default: ARCHIVE or RELEASE or tip)
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   876
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   877
  Build Isabelle release in base directory, using the local repository clone.
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   878
""",
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64371
diff changeset
   879
        "A:" -> (arg => afp_rev = arg),
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69432
diff changeset
   880
        "C:" -> (arg => components_base = Path.explode(arg)),
73607
fc13738e1933 clarified command-line, following other build_XYZ tools;
wenzelm
parents: 73582
diff changeset
   881
        "D:" -> (arg => target_dir = Path.explode(arg)),
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   882
        "R:" -> (arg => release_name = arg),
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   883
        "S:" -> (arg => source_archive = arg),
64211
1306a0e7fe81 explicit website directory;
wenzelm
parents: 64210
diff changeset
   884
        "W:" -> (arg => website = Some(Path.explode(arg))),
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   885
        "b:" -> (arg => build_sessions = space_explode(',', arg)),
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   886
        "c:" -> (arg =>
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   887
          {
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   888
            val path = Path.explode(arg)
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   889
            Components.Archive.get_name(path.file_name)
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   890
            more_components = more_components ::: List(path)
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69411
diff changeset
   891
          }),
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   892
        "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
64316
96fef7745c68 build HTML library in Isabelle/Scala;
wenzelm
parents: 64304
diff changeset
   893
        "l" -> (_ => build_library = true),
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69400
diff changeset
   894
        "o:" -> (arg => options = options + arg),
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69406
diff changeset
   895
        "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)),
64204
db9ac35cae0d added option -p for platform families;
wenzelm
parents: 64203
diff changeset
   896
        "r:" -> (arg => rev = arg))
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   897
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   898
      val more_args = getopts(args)
73607
fc13738e1933 clarified command-line, following other build_XYZ tools;
wenzelm
parents: 73582
diff changeset
   899
      if (more_args.nonEmpty) getopts.usage()
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   900
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   901
      if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   902
        error("Building for windows requires 7z")
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   903
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   904
      def make_context(name: String): Release_Context =
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   905
        Release_Context(target_dir,
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   906
          release_name = name,
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   907
          components_base = components_base,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   908
          progress = new Console_Progress())
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   909
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   910
      val context =
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   911
        if (source_archive.isEmpty) {
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   912
          val context = make_context(release_name)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   913
          val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   914
          build_release_archive(context, version, parallel_jobs = parallel_jobs)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   915
          context
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   916
        }
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   917
        else {
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   918
          val archive = Release_Archive.get(source_archive, rename = release_name)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   919
          val context = make_context(proper_string(release_name) getOrElse archive.identifier)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   920
          Isabelle_System.new_directory(context.dist_dir)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   921
          use_release_archive(context, archive, id = rev)
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   922
          context
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   923
        }
69415
99c3529c31d0 clarified error;
wenzelm
parents: 69414
diff changeset
   924
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73626
diff changeset
   925
      build_release(options, context, afp_rev = afp_rev,
64204
db9ac35cae0d added option -p for platform families;
wenzelm
parents: 64203
diff changeset
   926
        platform_families =
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   927
          if (platform_families.isEmpty) default_platform_families
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69167
diff changeset
   928
          else platform_families,
70101
4ae335fd3a54 option for build_sessions;
wenzelm
parents: 70099
diff changeset
   929
        more_components = more_components, build_sessions = build_sessions,
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73610
diff changeset
   930
        build_library = build_library, parallel_jobs = parallel_jobs, website = website)
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   931
    }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   932
  }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   933
}