# HG changeset patch # User wenzelm # Date 1540200878 -7200 # Node ID 822726043e281543b1295fa90045ca12c93baa7c # Parent 38beaaebe736368e0bed800469eb4d0414ed90e2 misc tuning and clarification; diff -r 38beaaebe736 -r 822726043e28 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Sun Oct 21 23:02:52 2018 +0100 +++ b/src/Pure/Admin/build_release.scala Mon Oct 22 11:34:38 2018 +0200 @@ -9,6 +9,49 @@ object Build_Release { + /** release info **/ + + sealed case class Bundle_Info( + platform_family: String, + platform_description: String, + main: String, + fallback: Option[String]) + { + def names: List[String] = main :: fallback.toList + } + + class Release private[Build_Release]( + val date: Date, + val dist_name: String, + val dist_dir: Path, + val dist_version: String, + val ident: String) + { + val isabelle_dir: Path = dist_dir + Path.explode(dist_name) + val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz") + val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") + + val other_isabelle_identifier: String = dist_name + "-build" + + val bundle_infos: List[Bundle_Info] = + List(Bundle_Info("linux", "Linux", dist_name + "_app.tar.gz", None), + Bundle_Info("windows", "Windows", dist_name + ".exe", None), + Bundle_Info("macos", "Mac OS X", dist_name + ".dmg", Some(dist_name + "_dmg.tar.gz"))) + + def read_ident(): String = + Isabelle_System.with_tmp_dir("build_release")(tmp_dir => + { + val getsettings = Path.explode(dist_name + "/" + getsettings_file) + execute_tar(tmp_dir, + "-xzf " + File.bash_path(isabelle_archive) + " " + File.bash_path(getsettings)) + split_lines(File.read(tmp_dir + getsettings)) + .collectFirst({ case ISABELLE_ID(ident) => ident }) + .getOrElse(error("Failed to read ISABELLE_ID from " + isabelle_archive)) + }) + } + + + /** generated content **/ /* patch release */ @@ -23,9 +66,10 @@ private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r - def patch_release( - dir: Path, ident: String, is_official: Boolean, dist_name: String, dist_version: String) + def patch_release(release: Release, is_official: Boolean) { + val dir = release.isabelle_dir + for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala")) { change_file(dir, name, @@ -36,11 +80,11 @@ change_file(dir, getsettings_file, s => - s.replaceAll("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(ident)) - .replaceAll("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(dist_name))) + s.replaceAll("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident)) + .replaceAll("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(release.dist_name))) change_file(dir, "lib/html/library_index_header.template", - s => s.replaceAll("""\{ISABELLE\}""", dist_name)) + s => s.replaceAll("""\{ISABELLE\}""", release.dist_name)) for { name <- @@ -49,24 +93,24 @@ "src/Pure/System/distribution.scala", "lib/Tools/version") } { - change_file(dir, name, s => s.replaceAll("repository version", dist_version)) + change_file(dir, name, s => s.replaceAll("repository version", release.dist_version)) } change_file(dir, "README", - s => s.replaceAll("some repository version of Isabelle", dist_version)) + s => s.replaceAll("some repository version of Isabelle", release.dist_version)) } /* ANNOUNCE */ - def make_announce(dir: Path, ident: String) + def make_announce(release: Release) { - File.write(dir + Path.explode("ANNOUNCE"), + File.write(release.isabelle_dir + Path.explode("ANNOUNCE"), """ IMPORTANT NOTE ============== -This is a snapshot of Isabelle/""" + ident + """ from the repository. +This is a snapshot of Isabelle/""" + release.ident + """ from the repository. """) } @@ -108,48 +152,6 @@ /** build_release **/ - sealed case class Bundle_Info( - platform_family: String, - platform_description: String, - main: String, - fallback: Option[String]) - { - def names: List[String] = main :: fallback.toList - } - - class Release private[Build_Release](val date: Date, val dist_name: String, val dist_dir: Path) - { - val isabelle_dir: Path = dist_dir + Path.explode(dist_name) - val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz") - val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") - - val other_isabelle_identifier: String = dist_name + "-build" - - val bundle_infos: List[Bundle_Info] = - List(Bundle_Info("linux", "Linux", dist_name + "_app.tar.gz", None), - Bundle_Info("windows", "Windows", dist_name + ".exe", None), - Bundle_Info("macos", "Mac OS X", dist_name + ".dmg", Some(dist_name + "_dmg.tar.gz"))) - - def bundle_info(platform_family: String): Bundle_Info = - bundle_infos.find(bundle_info => bundle_info.platform_family == platform_family) getOrElse - error("Unknown platform family " + quote(platform_family)) - - def read_ident(): String = - Isabelle_System.with_tmp_dir("build_release")(tmp_dir => - { - val getsettings = Path.explode(dist_name + "/" + getsettings_file) - execute_tar(tmp_dir, - "-xzf " + File.bash_path(isabelle_archive) + " " + File.bash_path(getsettings)) - split_lines(File.read(tmp_dir + getsettings)) - .collectFirst({ case ISABELLE_ID(ident) => ident }) - .getOrElse(error("Failed to read ISABELLE_ID from " + isabelle_archive)) - }) - - def execute_dist_name(dir: Path, script: String): Unit = - Isabelle_System.bash(script, cwd = dir.file, - env = Isabelle_System.settings() + ("DIST_NAME" -> dist_name)).check - } - private def execute(dir: Path, script: String): Unit = Isabelle_System.bash(script, cwd = dir.file).check @@ -159,7 +161,6 @@ private def tar_options: String = if (Platform.is_macos) "--owner=root --group=staff" else "--owner=root --group=root" - private val default_platform_families = List("linux", "windows", "macos") def build_release(base_dir: Path, @@ -174,12 +175,26 @@ parallel_jobs: Int = 1, remote_mac: String = ""): Release = { + val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME")) + val release = { val date = Date.now() val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date)) val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute - new Release(date, dist_name, dist_dir) + + val version = proper_release_name orElse proper_string(rev) getOrElse "tip" + val ident = + try { hg.id(version) } + catch { case ERROR(_) => error("Bad repository version: " + quote(version)) } + + val dist_version = + proper_release_name match { + case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date) + case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date) + } + + new Release(date, dist_name, dist_dir, dist_version, ident) } @@ -193,28 +208,13 @@ Isabelle_System.mkdirs(release.dist_dir) - val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME")) - val version = proper_release_name orElse proper_string(rev) getOrElse "tip" - val ident = - try { hg.id(version) } - catch { case ERROR(_) => error("Bad repository version: " + quote(version)) } - - val dist_version = - if (proper_release_name.isDefined) { - proper_release_name.get + ": " + Date.Format("LLLL uuuu")(release.date) - } - else "Isabelle repository snapshot " + ident + " " + Date.Format.date(release.date) - if (release.isabelle_dir.is_dir) error("Directory " + release.isabelle_dir + " already exists") - progress.echo("### Retrieving Mercurial repository version " + quote(version)) + progress.echo("### Retrieving Mercurial repository version " + quote(release.ident)) - try { - hg.archive(release.isabelle_dir.expand.implode, rev = ident, options = "--type files") - } - catch { case ERROR(_) => error("Failed to retrieve " + version + "(" + ident + ")") } + hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files") for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) { (release.isabelle_dir + Path.explode(name)).file.delete @@ -223,10 +223,9 @@ progress.echo("### Preparing distribution " + quote(release.dist_name)) - patch_release(release.isabelle_dir, ident, - proper_release_name.isDefined && official_release, release.dist_name, dist_version) + patch_release(release, proper_release_name.isDefined && official_release) - if (proper_release_name.isEmpty) make_announce(release.isabelle_dir, ident) + if (proper_release_name.isEmpty) make_announce(release) make_contrib(release.isabelle_dir) @@ -258,7 +257,7 @@ } catch { case ERROR(_) => error("Failed to build documentation") } - make_news(other_isabelle, dist_version) + make_news(other_isabelle, release.dist_version) for (name <- List("Admin", "browser_info", "heaps")) { Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name)) @@ -269,7 +268,11 @@ progress.echo("### Creating distribution archive " + release.isabelle_archive) - release.execute_dist_name(release.dist_dir, """ + def execute_dist_name(script: String): Unit = + Isabelle_System.bash(script, cwd = release.dist_dir.file, + env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check + + execute_dist_name(""" set -e chmod -R a+r "$DIST_NAME" @@ -281,7 +284,7 @@ execute_tar(release.dist_dir, tar_options + " -czf " + File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name)) - release.execute_dist_name(release.dist_dir, """ + execute_dist_name(""" set -e mv "$DIST_NAME" "${DIST_NAME}-old" @@ -305,7 +308,10 @@ /* make application bundles */ - val bundle_infos = platform_families.map(release.bundle_info(_)) + val bundle_infos = + platform_families.map(family => + release.bundle_infos.find(info => info.platform_family == family) getOrElse + error("Unknown platform family " + quote(family))) for (bundle_info <- bundle_infos) { val bundle =