support for existing release archive;
authorwenzelm
Wed, 05 May 2021 14:07:25 +0200
changeset 73885 a771807df752
parent 73884 ac8feb094bd4
child 73886 f2e836e013cb
support for existing release archive; misc tuning and clarification;
src/Pure/Admin/build_release.scala
src/Pure/Admin/isabelle_devel.scala
--- a/src/Pure/Admin/build_release.scala	Wed May 05 13:30:11 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed May 05 14:07:25 2021 +0200
@@ -11,6 +11,12 @@
 {
   /** release context **/
 
+  private def execute(dir: Path, script: String): Unit =
+    Isabelle_System.bash(script, cwd = dir.file).check
+
+  private def execute_tar(dir: Path, args: String, strip: Int = 0): Unit =
+    Isabelle_System.gnutar(args, dir = dir, strip = strip).check
+
   object Release_Context
   {
     def apply(
@@ -37,7 +43,7 @@
 
     val isabelle: Path = Path.explode(dist_name)
     val isabelle_dir: Path = dist_dir + isabelle
-    val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
+    val isabelle_archive: Path = dist_dir + isabelle.tar.gz
     val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
 
     def other_isabelle(dir: Path): Other_Isabelle =
@@ -88,30 +94,50 @@
 
   /** release archive **/
 
+  val ISABELLE: Path = Path.basic("Isabelle")
   val ISABELLE_ID: Path = Path.explode("etc/ISABELLE_ID")
   val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS")
   val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER")
 
   object Release_Archive
   {
-    def make(bytes: Bytes): Release_Archive =
+    def make(bytes: Bytes, rename: String = ""): Release_Archive =
     {
       Isabelle_System.with_tmp_dir("tmp")(dir =>
         Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
         {
+          val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
+
           Bytes.write(archive_path, bytes)
-          Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path),
-            dir = dir, original_owner = true, strip = 1).check
+          execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1)
+
+          val id = File.read(isabelle_dir + ISABELLE_ID)
+          val tags = File.read(isabelle_dir + ISABELLE_TAGS)
+          val identifier = File.read(isabelle_dir + ISABELLE_IDENTIFIER)
 
-          val id = File.read(dir + ISABELLE_ID)
-          val tags = File.read(dir + ISABELLE_TAGS)
-          val identifier = File.read(dir + ISABELLE_IDENTIFIER)
-          new Release_Archive(bytes, id, tags, identifier)
+          val (bytes1, identifier1) =
+            if (rename.isEmpty || rename == identifier) (bytes, identifier)
+            else {
+              File.write(isabelle_dir + ISABELLE_IDENTIFIER, rename)
+              Isabelle_System.move_file(isabelle_dir, dir + Path.basic(rename))
+              execute_tar(dir, "-czf " + File.bash_path(archive_path) + " " + Bash.string(rename))
+              (Bytes.read(archive_path), rename)
+            }
+          new Release_Archive(bytes1, id, tags, identifier1)
         })
       )
     }
 
-    def read(path: Path): Release_Archive = make(Bytes.read(path))
+    def read(path: Path, rename: String = ""): Release_Archive =
+      make(Bytes.read(path), rename = rename)
+
+    def get(url: String, rename: String = "", progress: Progress = new Progress): Release_Archive =
+    {
+      val bytes =
+        if (Path.is_wellformed(url)) Bytes.read(Path.explode(url))
+        else Isabelle_System.download(url, progress = progress).bytes
+      make(bytes, rename = rename)
+    }
   }
 
   case class Release_Archive private[Build_Release](
@@ -197,13 +223,6 @@
 
   /** build release **/
 
-  private def execute(dir: Path, script: String): Unit =
-    Isabelle_System.bash(script, cwd = dir.file).check
-
-  private def execute_tar(dir: Path, args: String): Unit =
-    Isabelle_System.gnutar(args, dir = dir).check
-
-
   /* build heaps on remote server */
 
   private def remote_build_heaps(
@@ -367,10 +386,24 @@
   private val default_platform_families: List[Platform.Family.Value] =
     List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
 
+  def use_release_archive(
+    context: Release_Context,
+    archive: Release_Archive,
+    id: String = ""): Unit =
+  {
+    if (id.nonEmpty && id != archive.id) {
+      error("Mismatch of release identification " + id + " vs. archive " + archive.id)
+    }
+
+    if (!context.isabelle_archive.is_file || Bytes.read(context.isabelle_archive) != archive.bytes) {
+      Bytes.write(context.isabelle_archive, archive.bytes)
+    }
+  }
+
   def build_release_archive(
     context: Release_Context,
     version: String,
-    parallel_jobs: Int = 1): Release_Archive =
+    parallel_jobs: Int = 1): Unit =
   {
     val progress = context.progress
 
@@ -381,10 +414,7 @@
 
     if (context.isabelle_archive.is_file) {
       progress.echo_warning("Found existing release archive: " + context.isabelle_archive)
-
-      val archive = Release_Archive.read(context.isabelle_archive)
-      if (id == archive.id) archive
-      else error("Mismatch of release identification " + id + " vs. archive " + archive.id)
+      use_release_archive(context, Release_Archive.read(context.isabelle_archive), id = id)
     }
     else {
       progress.echo_warning("Preparing release " + context.dist_name + " ...")
@@ -449,15 +479,12 @@
         """find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""")
       execute_tar(context.dist_dir, "-czf " +
         File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name))
-
-      Release_Archive.read(context.isabelle_archive)
     }
   }
 
   def build_release(
     options: Options,
     context: Release_Context,
-    release_archive: Release_Archive,
     afp_rev: String = "",
     platform_families: List[Platform.Family.Value] = default_platform_families,
     more_components: List[Path] = Nil,
@@ -471,22 +498,23 @@
 
     /* release directory */
 
-    for (name <- List(context.dist_name, "Isabelle")) {
-      Isabelle_System.rm_tree(context.dist_dir + Path.explode(name))
+    val archive = Release_Archive.read(context.isabelle_archive)
+
+    for (path <- List(context.isabelle, ISABELLE)) {
+      Isabelle_System.rm_tree(context.dist_dir + path)
     }
 
     Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
     {
-      Bytes.write(archive_path, release_archive.bytes)
+      Bytes.write(archive_path, archive.bytes)
       val extract =
         List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc").
-          map(name => context.dist_name + "/" + name)
+          map(name => context.release_name + "/" + name)
       execute_tar(context.dist_dir,
         "-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract))
     })
 
-    Isabelle_System.symlink(
-      Path.explode(context.dist_name), context.dist_dir + Path.explode("Isabelle"))
+    Isabelle_System.symlink(Path.explode(context.dist_name), context.dist_dir + ISABELLE)
 
 
     /* make application bundles */
@@ -614,7 +642,7 @@
             }
 
             make_isabelle_plist(
-              app_contents + Path.explode("Info.plist"), isabelle_name, release_archive.id)
+              app_contents + Path.explode("Info.plist"), isabelle_name, archive.id)
 
             make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component,
               classpath, dock_icon = true)
@@ -747,8 +775,8 @@
         } yield (bundle_info.name, bundle_info)
 
       val isabelle_link =
-        HTML.link(Isabelle_System.isabelle_repository.changeset(release_archive.id),
-          HTML.text("Isabelle/" + release_archive.id))
+        HTML.link(Isabelle_System.isabelle_repository.changeset(archive.id),
+          HTML.text("Isabelle/" + archive.id))
       val afp_link =
         HTML.link(Isabelle_System.afp_repository.changeset(afp_rev),
           HTML.text("AFP/" + afp_rev))
@@ -817,6 +845,7 @@
       var components_base: Path = Components.default_components_base
       var target_dir = Path.current
       var release_name = ""
+      var source_archive = ""
       var website: Option[Path] = None
       var build_sessions: List[String] = Nil
       var more_components: List[Path] = Nil
@@ -835,6 +864,7 @@
         Components.default_components_base + """)
     -D DIR       target directory (default ".")
     -R RELEASE   explicit release name
+    -S ARCHIVE   use existing source archive (file or URL)
     -W WEBSITE   produce minimal website in given directory
     -b SESSIONS  build platform-specific session images (separated by commas)
     -c ARCHIVE   clean bundling with additional component .tar.gz archive
@@ -842,7 +872,7 @@
     -l           build library
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p NAMES     platform families (default: """ + default_platform_families.mkString(",") + """)
-    -r REV       Mercurial changeset id (default: RELEASE or tip)
+    -r REV       Mercurial changeset id (default: ARCHIVE or RELEASE or tip)
 
   Build Isabelle release in base directory, using the local repository clone.
 """,
@@ -850,6 +880,7 @@
         "C:" -> (arg => components_base = Path.explode(arg)),
         "D:" -> (arg => target_dir = Path.explode(arg)),
         "R:" -> (arg => release_name = arg),
+        "S:" -> (arg => source_archive = arg),
         "W:" -> (arg => website = Some(Path.explode(arg))),
         "b:" -> (arg => build_sessions = space_explode(',', arg)),
         "c:" -> (arg =>
@@ -867,19 +898,31 @@
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
-      val context =
+      if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
+        error("Building for windows requires 7z")
+
+      def make_context(name: String): Release_Context =
         Release_Context(target_dir,
-          release_name = release_name,
+          release_name = name,
           components_base = components_base,
           progress = new Console_Progress())
 
-      if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
-        error("Building for windows requires 7z")
+      val context =
+        if (source_archive.isEmpty) {
+          val context = make_context(release_name)
+          val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
+          build_release_archive(context, version, parallel_jobs = parallel_jobs)
+          context
+        }
+        else {
+          val archive = Release_Archive.get(source_archive, rename = release_name)
+          val context = make_context(proper_string(release_name) getOrElse archive.identifier)
+          Isabelle_System.new_directory(context.dist_dir)
+          use_release_archive(context, archive, id = rev)
+          context
+        }
 
-      val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
-      val release_archive = build_release_archive(context, version, parallel_jobs = parallel_jobs)
-
-      build_release(options, context, release_archive, afp_rev = afp_rev,
+      build_release(options, context, afp_rev = afp_rev,
         platform_families =
           if (platform_families.isEmpty) default_platform_families
           else platform_families,
--- a/src/Pure/Admin/isabelle_devel.scala	Wed May 05 13:30:11 2021 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala	Wed May 05 14:07:25 2021 +0200
@@ -42,8 +42,8 @@
           website_dir =>
         {
           val context = Build_Release.Release_Context(target_dir)
-          val release_archive = Build_Release.build_release_archive(context, rev)
-          Build_Release.build_release(options, context, release_archive, afp_rev = afp_rev,
+          Build_Release.build_release_archive(context, rev)
+          Build_Release.build_release(options, context, afp_rev = afp_rev,
             build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
             website = Some(website_dir))
         })