# HG changeset patch # User wenzelm # Date 1620216445 -7200 # Node ID a771807df7520a697d4ebf825c005de99fd46c4e # Parent ac8feb094bd448386d359814748c9c1302a6eb85 support for existing release archive; misc tuning and clarification; diff -r ac8feb094bd4 -r a771807df752 src/Pure/Admin/build_release.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, diff -r ac8feb094bd4 -r a771807df752 src/Pure/Admin/isabelle_devel.scala --- 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)) })