--- 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 =