src/Pure/Admin/build_release.scala
author wenzelm
Fri, 14 Oct 2016 16:53:26 +0200
changeset 64203 2f9a1c76f731
parent 64202 967515846691
child 64204 db9ac35cae0d
permissions -rw-r--r--
more formal Release_Info; more incremental treatment of additional builds (bundles, library); tuned;
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
{
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    12
  sealed case class Release_Info(
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    13
    date: Date, name: String, dist_dir: Path, dist_archive: Path, dist_library_archive: Path)
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    14
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    15
  def build_release(base_dir: Path,
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    16
    progress: Progress = Ignore_Progress,
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    17
    rev: String = "",
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    18
    official_release: Boolean = false,
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    19
    release_name: String = "",
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    20
    build_library: Boolean = false,
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    21
    parallel_jobs: Int = 1,
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    22
    remote_mac: String = ""): Release_Info =
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    23
  {
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    24
    /* release info */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    25
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    26
    val release_info =
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    27
    {
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    28
      val date = Date.now()
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    29
      val name = if (release_name != "") release_name else "Isabelle_" + Date.Format.date(date)
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    30
      val dist_dir = base_dir + Path.explode("dist-" + name)
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    31
      val dist_archive = dist_dir + Path.explode(name + ".tar.gz")
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    32
      val dist_library_archive = dist_dir + Path.explode(name + "_library.tar.gz")
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    33
      Release_Info(date, name, dist_dir, dist_archive, dist_library_archive)
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    34
    }
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    35
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    36
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    37
    /* make distribution */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    38
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    39
    val jobs_option = " -j" + parallel_jobs.toString
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    40
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    41
    if (release_info.dist_archive.is_file)
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    42
      progress.echo("Release archive " + release_info.dist_archive + " already exists")
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    43
    else {
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    44
      progress.echo("Producing release archive " + release_info.dist_archive + " ...")
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    45
      progress.bash(
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    46
        "isabelle makedist -d " + File.bash_path(base_dir) + jobs_option +
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    47
          (if (official_release) " -O" else "") +
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    48
          (if (release_name != "") " -r " + File.bash_string(release_name) else "") +
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    49
          (if (rev != "") " " + File.bash_string(rev) else ""),
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    50
        echo = true).check
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    51
    }
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    52
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    53
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    54
    /* make application bundles */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    55
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    56
    val platform_bundles =
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    57
      List("linux" -> (release_info.name + "_app.tar.gz"),
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    58
        "windows" -> (release_info.name + "-win32.exe"),
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    59
        "windows64" -> (release_info.name + "-win64.exe"),
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    60
        "macos" -> (release_info.name + ".dmg"))
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    61
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    62
    for ((platform_family, bundle) <- platform_bundles) {
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    63
      val bundle_archive =
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    64
        release_info.dist_dir +
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    65
          Path.explode(
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    66
            if (platform_family == "macos" && remote_mac.isEmpty)
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    67
              release_info.name + "_dmg.tar.gz"
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    68
            else bundle)
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    69
      if (bundle_archive.is_file)
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    70
        progress.echo("Application bundle " + bundle_archive + " already exists")
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    71
      else {
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    72
        progress.echo("\n*** " + platform_family + ": " + bundle_archive + " ***")
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    73
        progress.bash(
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    74
          "isabelle makedist_bundle " + File.bash_path(release_info.dist_archive) +
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    75
            " " + File.bash_string(platform_family) +
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    76
            (if (remote_mac == "") "" else " " + File.bash_string(remote_mac)),
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    77
          echo = true).check
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    78
      }
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    79
    }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    80
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    81
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    82
    /* minimal website */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    83
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    84
    File.write(release_info.dist_dir + Path.explode("index.html"),
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    85
"""<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 3.2//EN">
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    86
<html>
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    87
<head>
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    88
<title>""" + HTML.output(release_info.name) + """</title>
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    89
</head>
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    90
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    91
<body>
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    92
<h1>""" + HTML.output(release_info.name) + """</h1>
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    93
<ul>
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    94
""" +
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    95
  cat_lines(platform_bundles.map({ case (a, b) =>
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    96
    "<li><a href=" + quote(HTML.output(a)) + ">" + HTML.output(b) + "</a></li>" })) +
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
    97
"""
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    98
</ul>
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
    99
</body>
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   100
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   101
</html>
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   102
""")
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   103
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   104
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   105
    /* HTML library */
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   106
64203
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   107
    if (build_library) {
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   108
      if (release_info.dist_library_archive.is_file)
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   109
        progress.echo("Library archive " + release_info.dist_library_archive + " already exists")
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   110
      else {
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   111
        progress.bash("\"$ISABELLE_HOME/Admin/Release/build_library\"" + jobs_option + " " +
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   112
          File.bash_path(release_info.dist_dir +
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   113
            Path.explode(release_info.name + "_" +
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   114
              Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY") + ".tar.gz"))).check
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   115
      }
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   116
    }
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   117
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   118
2f9a1c76f731 more formal Release_Info;
wenzelm
parents: 64202
diff changeset
   119
    release_info
64202
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   120
  }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   121
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   122
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   123
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   124
  /** command line entry point **/
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   125
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   126
  def main(args: Array[String])
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   127
  {
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   128
    Command_Line.tool0 {
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   129
      var remote_mac = ""
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   130
      var official_release = false
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   131
      var release_name = ""
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   132
      var parallel_jobs = 1
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   133
      var build_library = false
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   134
      var rev = ""
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   135
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   136
      val getopts = Getopts("""
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   137
Usage: Admin/build_release [OPTIONS] BASE_DIR
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   138
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   139
  Options are:
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   140
    -M USER@HOST remote Mac OS X for dmg build
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   141
    -O           official release (not release-candidate)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   142
    -R RELEASE   proper release with name
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   143
    -j INT       maximum number of parallel jobs (default 1)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   144
    -l           build library
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   145
    -r REV       Mercurial changeset id (default: RELEASE or tip)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   146
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   147
  Build Isabelle release in base directory, using the local repository clone.
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   148
""",
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   149
        "M:" -> (arg => remote_mac = arg),
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   150
        "O" -> (_ => official_release = true),
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   151
        "R:" -> (arg => release_name = arg),
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   152
        "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   153
        "l" -> (_ => build_library))
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   154
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   155
      val more_args = getopts(args)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   156
      val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   157
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   158
      val progress = new Console_Progress()
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   159
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   160
      build_release(Path.explode(base_dir), progress = progress, rev = rev,
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   161
        official_release = official_release, release_name = release_name,
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   162
        build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac)
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   163
    }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   164
  }
967515846691 replaced shell script by Isabelle/Scala;
wenzelm
parents:
diff changeset
   165
}