# HG changeset patch
# User wenzelm
# Date 1540147467 -7200
# Node ID 710845a859449c19f478b143119daf2fe85ee460
# Parent  6d28536481ad3a4c242f3516003a3cf49f16fd25
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;

diff -r 6d28536481ad -r 710845a85944 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Sun Oct 21 19:39:46 2018 +0200
+++ b/src/Pure/Admin/build_release.scala	Sun Oct 21 20:44:27 2018 +0200
@@ -19,6 +19,10 @@
     File.write(file, f(File.read(file)))
   }
 
+  private val getsettings_file: String = "lib/scripts/getsettings"
+
+  private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r
+
   def patch_release(
     dir: Path, ident: String, is_official: Boolean, dist_name: String, dist_version: String)
   {
@@ -30,7 +34,7 @@
            .replaceAll("val is_official = false", "val is_official = " + is_official))
     }
 
-    change_file(dir, "lib/scripts/getsettings",
+    change_file(dir, getsettings_file,
       s =>
         s.replaceAll("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(ident))
          .replaceAll("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(dist_name)))
@@ -113,11 +117,7 @@
     def names: List[String] = main :: fallback.toList
   }
 
-  sealed case class Release(
-    date: Date,
-    dist_name: String,
-    dist_dir: Path,
-    ident: String)
+  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")
@@ -134,6 +134,17 @@
       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
@@ -163,114 +174,102 @@
     parallel_jobs: Int = 1,
     remote_mac: String = ""): Release =
   {
-    /* make distribution */
-
     val release =
     {
-      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
-        Release(date, dist_name, dist_dir, "")
-      }
+      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)
+    }
+
+
+    /* make distribution */
 
-      val isabelle_ident_file = base_dir + Path.explode("ISABELLE_IDENT")
-      val isabelle_dist_file = base_dir + Path.explode("ISABELLE_DIST")
+    if (release.isabelle_archive.is_file) {
+      progress.echo("### Release archive already exists: " + release.isabelle_archive.implode)
+    }
+    else {
+      progress.echo("### Producing release archive " + release.isabelle_archive.implode + " ...")
+
+      Isabelle_System.mkdirs(release.dist_dir)
 
-      val release_ident =
-        if (release.isabelle_archive.is_file &&
-            isabelle_ident_file.is_file && isabelle_dist_file.is_file &&
-            File.eq(Path.explode(Library.trim_line(File.read(isabelle_dist_file))),
-              release.isabelle_archive)) {
-          progress.echo("### Release archive already exists: " + release.isabelle_archive.implode)
-          File.read(isabelle_ident_file)
+      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 {
-          progress.echo("Producing release archive " + release.isabelle_archive.implode + " ...")
-
-          Isabelle_System.mkdirs(release.dist_dir)
+        else "Isabelle repository snapshot " + ident + " " + Date.Format.date(release.date)
 
-          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)) }
+      if (release.isabelle_dir.is_dir)
+        error("Directory " + release.isabelle_dir + " already exists")
+
+
+      progress.echo("### Retrieving Mercurial 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)
+      try {
+        hg.archive(release.isabelle_dir.expand.implode, rev = ident, options = "--type files")
+      }
+      catch { case ERROR(_) => error("Failed to retrieve " + version + "(" + ident + ")") }
 
-          if (release.isabelle_dir.is_dir)
-            error("Directory " + release.isabelle_dir + " already exists")
-
-          isabelle_ident_file.file.delete
-          isabelle_dist_file.file.delete
+      for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
+        (release.isabelle_dir + Path.explode(name)).file.delete
+      }
 
 
-          progress.echo("### Retrieving Mercurial repository version " + quote(version))
+      progress.echo("### Preparing distribution " + quote(release.dist_name))
 
-          try {
-            hg.archive(release.isabelle_dir.expand.implode, rev = ident, options = "--type files")
-          }
-          catch { case ERROR(_) => error("Failed to retrieve " + version + "(" + ident + ")") }
-
-          for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
-            (release.isabelle_dir + Path.explode(name)).file.delete
-          }
+      patch_release(release.isabelle_dir, ident,
+        proper_release_name.isDefined && official_release, release.dist_name, dist_version)
 
-
-          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)
+      if (proper_release_name.isEmpty) make_announce(release.isabelle_dir, ident)
 
-          if (proper_release_name.isEmpty) make_announce(release.isabelle_dir, ident)
+      make_contrib(release.isabelle_dir)
 
-          make_contrib(release.isabelle_dir)
-
-          execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
+      execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
 
 
-          /* build tools and documentation */
+      /* build tools and documentation */
 
-          val other_isabelle =
-            Other_Isabelle(release.isabelle_dir,
-              isabelle_identifier = release.other_isabelle_identifier,
-              progress = progress)
+      val other_isabelle =
+        Other_Isabelle(release.isabelle_dir,
+          isabelle_identifier = release.other_isabelle_identifier,
+          progress = progress)
 
-          other_isabelle.init_settings(
-            (base_dir.absolute + Path.explode("contrib")).implode, nonfree = false, Nil)
-          other_isabelle.resolve_components(echo = true)
+      other_isabelle.init_settings(
+        (base_dir.absolute + Path.explode("contrib")).implode, nonfree = false, Nil)
+      other_isabelle.resolve_components(echo = true)
 
-          try {
-            val export_classpath =
-              "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
-            other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
-            other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
-          }
-          catch { case ERROR(_) => error("Failed to build tools") }
+      try {
+        val export_classpath =
+          "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
+        other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
+        other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
+      }
+      catch { case ERROR(_) => error("Failed to build tools") }
 
-          try {
-            other_isabelle.bash(
-              "./bin/isabelle build_doc -a -s -j " + parallel_jobs, echo = true).check
-          }
-          catch { case ERROR(_) => error("Failed to build documentation") }
+      try {
+        other_isabelle.bash(
+          "./bin/isabelle build_doc -a -s -j " + parallel_jobs, echo = true).check
+      }
+      catch { case ERROR(_) => error("Failed to build documentation") }
 
-          make_news(other_isabelle, dist_version)
+      make_news(other_isabelle, dist_version)
 
-          for (name <- List("Admin", "browser_info", "heaps")) {
-            Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
-          }
+      for (name <- List("Admin", "browser_info", "heaps")) {
+        Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
+      }
 
-          other_isabelle.cleanup()
+      other_isabelle.cleanup()
 
 
-          progress.echo("### Creating distribution archive " + release.isabelle_archive)
+      progress.echo("### Creating distribution archive " + release.isabelle_archive)
 
-          release.execute_dist_name(release.dist_dir, """
+      release.execute_dist_name(release.dist_dir, """
 set -e
 
 chmod -R a+r "$DIST_NAME"
@@ -279,10 +278,10 @@
 find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
 """)
 
-          execute_tar(release.dist_dir, tar_options + " -czf " +
-            File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
+      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, """
+      release.execute_dist_name(release.dist_dir, """
 set -e
 
 mv "$DIST_NAME" "${DIST_NAME}-old"
@@ -301,13 +300,6 @@
 
 rm -rf "${DIST_NAME}-old"
 """)
-
-          File.write(isabelle_dist_file, release.isabelle_archive.implode)
-          File.write(isabelle_ident_file, ident)
-          ident
-        }
-
-      release.copy(ident = release_ident)
     }
 
 
@@ -345,10 +337,12 @@
       val afp_link =
         HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev))
 
+      val ident = release.read_ident()
+
       HTML.write_document(dir, "index.html",
         List(HTML.title(release.dist_name)),
         List(
-          HTML.chapter(release.dist_name + " (" + release.ident + ")"),
+          HTML.chapter(release.dist_name + " (" + ident + ")"),
           HTML.itemize(
             website_platform_bundles.map({ case (bundle, bundle_info) =>
               List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) :::