# HG changeset patch # User wenzelm # Date 1674675744 -3600 # Node ID 023273cf26511c58cf98c57aba62f97864adf1f9 # Parent 940a6cb734fd7e03762d279effdbbd535c8d654b clean components more accurately: purge other platforms or archives; diff -r 940a6cb734fd -r 023273cf2651 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Wed Jan 25 20:38:38 2023 +0100 +++ b/src/Pure/Admin/build_release.scala Wed Jan 25 20:42:24 2023 +0100 @@ -610,7 +610,7 @@ // application bundling - Components.purge(contrib_dir, platform) + Components.clean_base(contrib_dir, platforms = List(platform), progress = progress) platform match { case Platform.Family.linux_arm | Platform.Family.linux => diff -r 940a6cb734fd -r 023273cf2651 src/Pure/Admin/other_isabelle.scala --- a/src/Pure/Admin/other_isabelle.scala Wed Jan 25 20:38:38 2023 +0100 +++ b/src/Pure/Admin/other_isabelle.scala Wed Jan 25 20:42:24 2023 +0100 @@ -89,10 +89,17 @@ "init_component " + quote(components_base) + "/" + name) } - def resolve_components(echo: Boolean = false): Unit = { + def resolve_components( + echo: Boolean = false, + clean_platforms: Option[List[Platform.Family.Value]] = None, + clean_archives: Boolean = false + ): Unit = { val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING")) for (path <- missing) { - Components.resolve(path.dir, path.file_name, ssh = ssh, + Components.resolve(path.dir, path.file_name, + clean_platforms = clean_platforms, + clean_archives = clean_archives, + ssh = ssh, progress = if (echo) progress else new Progress) } } @@ -142,15 +149,19 @@ def init( other_settings: List[String] = init_components(), fresh: Boolean = false, - echo: Boolean = false + echo: Boolean = false, + clean_platforms: Option[List[Platform.Family.Value]] = None, + clean_archives: Boolean = false ): Unit = { init_settings(other_settings) - resolve_components(echo = echo) + resolve_components( + echo = echo, + clean_platforms = clean_platforms, + clean_archives = clean_archives) scala_build(fresh = fresh, echo = echo) } - /* cleanup */ def cleanup(): Unit = { diff -r 940a6cb734fd -r 023273cf2651 src/Pure/System/components.scala --- a/src/Pure/System/components.scala Wed Jan 25 20:38:38 2023 +0100 +++ b/src/Pure/System/components.scala Wed Jan 25 20:42:24 2023 +0100 @@ -33,6 +33,30 @@ } + /* platforms */ + + private val family_platforms: Map[Platform.Family.Value, List[String]] = + Map( + Platform.Family.linux_arm -> List("arm64-linux", "arm64_32-linux"), + Platform.Family.linux -> List("x86_64-linux", "x86_64_32-linux"), + Platform.Family.macos -> + List("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), + Platform.Family.windows -> + List("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows")) + + private val platform_names: Set[String] = + Set("x86-linux", "x86-cygwin") ++ family_platforms.iterator.flatMap(_._2) + + def platform_purge(platforms: List[Platform.Family.Value]): String => Boolean = { + val preserve = + (for { + family <- platforms.iterator + platform <- family_platforms(family) + } yield platform).toSet + (name: String) => platform_names(name) && !preserve(name) + } + + /* component collections */ def default_component_repository: String = @@ -64,47 +88,73 @@ name } + def clean( + component_dir: Path, + platforms: List[Platform.Family.Value] = Platform.Family.list, + ssh: SSH.System = SSH.Local, + progress: Progress = new Progress + ): Unit = { + val purge = platform_purge(platforms) + for { + name <- ssh.read_dir(component_dir) + path = Path.basic(name) + if purge(name) && ssh.is_dir(component_dir + path) + } { + progress.echo("Removing " + (component_dir.base + path)) + ssh.rm_tree(component_dir + path) + } + } + + def clean_base( + base_dir: Path, + platforms: List[Platform.Family.Value] = Platform.Family.list, + ssh: SSH.System = SSH.Local, + progress: Progress = new Progress + ): Unit = { + for { + name <- ssh.read_dir(base_dir) + dir = base_dir + Path.basic(name) + if is_component_dir(dir) + } clean(dir, platforms = platforms, ssh = ssh, progress = progress) + } + def resolve( base_dir: Path, name: String, target_dir: Option[Path] = None, copy_dir: Option[Path] = None, + clean_platforms: Option[List[Platform.Family.Value]] = None, + clean_archives: Boolean = false, component_repository: String = Components.default_component_repository, ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): Unit = { ssh.make_directory(base_dir) + val archive_name = Archive(name) val archive = base_dir + Path.basic(archive_name) if (!ssh.is_file(archive)) { val remote = Url.append_path(component_repository, archive_name) ssh.download_file(remote, archive, progress = progress) } + for (dir <- copy_dir) { ssh.make_directory(dir) ssh.copy_file(archive, dir) } - unpack(target_dir getOrElse base_dir, archive, ssh = ssh, progress = progress) - } + + val unpack_dir = target_dir getOrElse base_dir + unpack(unpack_dir, archive, ssh = ssh, progress = progress) - private val platforms_family: Map[Platform.Family.Value, Set[String]] = - Map( - Platform.Family.linux_arm -> Set("arm64-linux", "arm64_32-linux"), - Platform.Family.linux -> Set("x86_64-linux", "x86_64_32-linux"), - Platform.Family.macos -> - Set("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), - Platform.Family.windows -> - Set("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows")) + if (clean_platforms.isDefined) { + clean(unpack_dir + Path.basic(name), + platforms = clean_platforms.get, ssh = ssh, progress = progress) + } - private val platforms_all: Set[String] = - Set("x86-linux", "x86-cygwin") ++ platforms_family.iterator.flatMap(_._2) - - def purge(dir: Path, platform: Platform.Family.Value): Unit = { - val purge_set = platforms_all -- platforms_family(platform) - - File.find_files(dir.file, - (file: JFile) => file.isDirectory && purge_set(file.getName), - include_dirs = true).foreach(Isabelle_System.rm_tree) + if (clean_archives) { + progress.echo("Removing " + quote(archive_name)) + ssh.delete(archive) + } } @@ -113,6 +163,10 @@ def directories(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS")) + def is_component_dir(dir: Path, ssh: SSH.System = SSH.Local): Boolean = + ssh.is_file(dir + Path.explode("etc/settings")) || + ssh.is_file(dir + Path.explode("etc/components")) + /* component directory content */