--- 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 =>
--- 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 = {
--- 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 */