# HG changeset patch # User wenzelm # Date 1544107471 -3600 # Node ID 52727566c1ba768cab1f2bf33e1482ee866f2a39 # Parent f0b85c8aec46c24ab67adb83a8eee3e096500e72 more explicit Components.Archive; support additional components, which also enforces clean bundling; diff -r f0b85c8aec46 -r 52727566c1ba src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Thu Dec 06 14:51:09 2018 +0100 +++ b/src/Pure/Admin/build_release.scala Thu Dec 06 15:44:31 2018 +0100 @@ -187,18 +187,20 @@ (components, jdk_component) } - def activate_bundled_components(dir: Path, platform: Platform.Family.Value) + def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String]) { + def contrib_name(name: String): String = + Components.contrib(name = name).implode + val Bundled = new Bundled(platform = Some(platform)) Components.write_components(dir, Components.read_components(dir).flatMap(line => line match { case Bundled(name) => - if (Components.check_dir(Components.contrib(dir, name))) - Some(Components.contrib(name = name).implode) + if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name)) else None case _ => if (Bundled.detect(line)) None else Some(line) - })) + }) ::: more_names.map(contrib_name(_))) } def make_contrib(dir: Path) @@ -236,6 +238,7 @@ official_release: Boolean = false, proper_release_name: Option[String] = None, platform_families: List[Platform.Family.Value] = default_platform_families, + more_components: List[Path] = Nil, website: Option[Path] = None, build_library: Boolean = false, parallel_jobs: Int = 1, @@ -395,7 +398,7 @@ val bundle = (if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main val bundle_archive = release.dist_dir + Path.explode(bundle) - if (bundle_archive.is_file) + if (bundle_archive.is_file && more_components.isEmpty) progress.echo_warning("Application bundle already exists: " + bundle_archive) else { val isabelle_name = release.dist_name @@ -418,14 +421,18 @@ val contrib_dir = Components.contrib(isabelle_target) - val (components, jdk_component) = get_bundled_components(isabelle_target, platform) + val (bundled_components, jdk_component) = + get_bundled_components(isabelle_target, platform) Components.resolve(other_isabelle.components_base(components_base), - components, target_dir = Some(contrib_dir), progress = progress) + bundled_components, target_dir = Some(contrib_dir), progress = progress) + + val more_components_names = + more_components.map(Components.unpack(contrib_dir, _, progress = progress)) Components.purge(contrib_dir, platform) - activate_bundled_components(isabelle_target, platform) + activate_components(isabelle_target, platform, more_components_names) // Java parameters @@ -736,6 +743,7 @@ var official_release = false var proper_release_name: Option[String] = None var website: Option[Path] = None + var more_components: List[Path] = Nil var parallel_jobs = 1 var build_library = false var options = Options.init() @@ -752,6 +760,7 @@ -O official release (not release-candidate) -R RELEASE proper release with name -W WEBSITE produce minimal website in given directory + -c ARCHIVE clean bundling with additional component .tar.gz archive -j INT maximum number of parallel jobs (default 1) -l build library -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) @@ -766,6 +775,12 @@ "O" -> (_ => official_release = true), "R:" -> (arg => proper_release_name = Some(arg)), "W:" -> (arg => website = Some(Path.explode(arg))), + "c:" -> (arg => + { + val path = Path.explode(arg) + Components.Archive.get_name(path.file_name) + more_components = more_components ::: List(path) + }), "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), "l" -> (_ => build_library = true), "o:" -> (arg => options = options + arg), @@ -783,7 +798,8 @@ platform_families = if (platform_families.isEmpty) default_platform_families else platform_families, - build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac) + more_components = more_components, build_library = build_library, + parallel_jobs = parallel_jobs, remote_mac = remote_mac) } } } diff -r f0b85c8aec46 -r 52727566c1ba src/Pure/System/components.scala --- a/src/Pure/System/components.scala Thu Dec 06 14:51:09 2018 +0100 +++ b/src/Pure/System/components.scala Thu Dec 06 15:44:31 2018 +0100 @@ -12,6 +12,19 @@ object Components { + /* archive name */ + + object Archive + { + val suffix: String = ".tar.gz" + def apply(name: String): String = name + suffix + def unapply(archive: String): Option[String] = Library.try_unsuffix(suffix, archive) + def get_name(archive: String): String = + unapply(archive) getOrElse + error("Bad component archive name (expecting .tar.gz): " + quote(archive)) + } + + /* component collections */ def admin(dir: Path): Path = dir + Path.explode("Admin/components") @@ -19,23 +32,28 @@ def contrib(dir: Path = Path.current, name: String = ""): Path = dir + Path.explode("contrib") + Path.explode(name) + def unpack(dir: Path, archive: Path, progress: Progress = No_Progress): String = + { + val name = Archive.get_name(archive.file_name) + progress.echo("Unpacking " + name) + Isabelle_System.gnutar("-C " + File.bash_path(dir) + " -xzf " + File.bash_path(archive)).check + name + } + def resolve(base_dir: Path, names: List[String], target_dir: Option[Path] = None, progress: Progress = No_Progress) { Isabelle_System.mkdirs(base_dir) for (name <- names) { - val archive_name = name + ".tar.gz" + val archive_name = Archive(name) val archive = base_dir + Path.explode(archive_name) if (!archive.is_file) { val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive_name progress.echo("Getting " + remote) Bytes.write(archive, Url.read_bytes(Url(remote))) } - progress.echo("Unpacking " + archive_name) - Isabelle_System.gnutar( - "-C " + File.bash_path(target_dir getOrElse base_dir) + - " -xzf " + File.bash_path(archive)).check + unpack(target_dir getOrElse base_dir, archive, progress = progress) } }