--- a/src/Pure/Admin/build_history.scala Wed Jan 25 13:37:44 2023 +0000
+++ b/src/Pure/Admin/build_history.scala Wed Jan 25 22:00:21 2023 +0100
@@ -104,6 +104,7 @@
isabelle_identifier: String = default_isabelle_identifier,
ml_statistics_step: Int = 1,
component_repository: String = Components.default_component_repository,
+ components_base: String = Components.standard_components_base,
fresh: Boolean = false,
hostname: String = "",
multicore_base: Boolean = false,
@@ -186,6 +187,7 @@
val component_settings =
other_isabelle.init_components(
component_repository = component_repository,
+ components_base = components_base,
catalogs = Components.optional_catalogs)
other_isabelle.init_settings(component_settings ::: init_settings)
other_isabelle.resolve_components(echo = verbose)
@@ -392,6 +394,7 @@
Command_Line.tool {
var afp = false
var multicore_base = false
+ var components_base = Components.standard_components_base
var heap: Option[Int] = None
var max_heap: Option[Int] = None
var multicore_list = List(default_multicore)
@@ -416,6 +419,8 @@
Options are:
-A include $ISABELLE_HOME/AFP directory
-B first multicore build serves as base for scheduling information
+ -C DIR base directory for Isabelle components (default: """ +
+ quote(Components.standard_components_base) + """)
-H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ +
default_heap * 2 + """ for x86_64)
-M MULTICORE multicore configurations (see below)
@@ -445,6 +450,7 @@
""",
"A" -> (_ => afp = true),
"B" -> (_ => multicore_base = true),
+ "C:" -> (arg => components_base = arg),
"H:" -> (arg => heap = Some(Value.Int.parse(arg))),
"M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)),
"N:" -> (arg => isabelle_identifier = arg),
@@ -481,7 +487,7 @@
local_build(Options.init(), root, progress = progress,
afp = afp, afp_partition = afp_partition,
isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
- component_repository = component_repository,
+ component_repository = component_repository, components_base = components_base,
fresh = fresh, hostname = hostname, multicore_base = multicore_base,
multicore_list = multicore_list, arch_64 = arch_64,
heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
@@ -545,9 +551,12 @@
strict = strict).check
sync(isabelle_self)
- execute("bin/isabelle", "components -I")
- execute("bin/isabelle", "components -a", echo = true)
- execute("bin/isabelle", "jedit -bf")
+
+ val self_isabelle =
+ Other_Isabelle(isabelle_self, isabelle_identifier = isabelle_identifier,
+ ssh = ssh, progress = progress)
+
+ self_isabelle.init(fresh = true, echo = true)
sync(isabelle_other, accurate = true,
rev = proper_string(rev) getOrElse "tip",
@@ -563,10 +572,15 @@
val output_file = tmp_dir + Path.explode("output")
val build_options = (if (afp_repos.isEmpty) "" else " -A") + " " + options
try {
- execute("Admin/build_other",
- "-o " + ssh.bash_path(output_file) + build_options + " " +
- ssh.bash_path(isabelle_other) + " " + args,
- echo = true, strict = false)
+ val script =
+ Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
+ ssh.bash_path(self_isabelle.isabelle_home + Path.explode("Admin/build_other")) +
+ " -o " + ssh.bash_path(output_file) + build_options + " " +
+ ssh.bash_path(isabelle_other) + " " + args
+ ssh.execute(script,
+ progress_stdout = progress.echo,
+ progress_stderr = progress.echo,
+ strict = false).check
}
catch {
case ERROR(msg) =>
@@ -577,7 +591,7 @@
yield {
val log = Path.explode(line)
val bytes = ssh.read_bytes(log)
- ssh.rm(log)
+ ssh.delete(log)
(log.file_name, bytes)
}
}
--- a/src/Pure/Admin/build_release.scala Wed Jan 25 13:37:44 2023 +0000
+++ b/src/Pure/Admin/build_release.scala Wed Jan 25 22:00:21 2023 +0100
@@ -464,10 +464,7 @@
val other_isabelle = context.other_isabelle(context.dist_dir)
- other_isabelle.init_settings(other_isabelle.init_components())
- other_isabelle.resolve_components(echo = true)
-
- other_isabelle.scala_build(echo = true)
+ other_isabelle.init(echo = true)
try {
other_isabelle.bash(
@@ -613,7 +610,7 @@
// application bundling
- Components.purge(contrib_dir, platform)
+ Components.clean_base(contrib_dir, platforms = List(platform))
platform match {
case Platform.Family.linux_arm | Platform.Family.linux =>
--- a/src/Pure/Admin/other_isabelle.scala Wed Jan 25 13:37:44 2023 +0000
+++ b/src/Pure/Admin/other_isabelle.scala Wed Jan 25 22:00:21 2023 +0100
@@ -10,24 +10,33 @@
object Other_Isabelle {
def apply(
- isabelle_home: Path,
+ root: Path,
isabelle_identifier: String = "",
+ ssh: SSH.System = SSH.Local,
progress: Progress = new Progress
): Other_Isabelle = {
- if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) {
- error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
- }
-
- new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, progress)
+ val (isabelle_home, url_prefix) =
+ ssh match {
+ case session: SSH.Session => (ssh.absolute_path(root), session.rsync_prefix)
+ case _ =>
+ if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) {
+ error("Cannot manage other Isabelle distribution: global ISABELLE_SETTINGS_PRESENT")
+ }
+ (root.canonical, "")
+ }
+ val isabelle_home_url = url_prefix + isabelle_home.implode
+ new Other_Isabelle(isabelle_home, isabelle_identifier, isabelle_home_url, ssh, progress)
}
}
final class Other_Isabelle private(
val isabelle_home: Path,
val isabelle_identifier: String,
+ isabelle_home_url: String,
+ ssh: SSH.System,
progress: Progress
) {
- override def toString: String = isabelle_home.toString
+ override def toString: String = isabelle_home_url
/* static system */
@@ -38,9 +47,14 @@
echo: Boolean = false,
strict: Boolean = true
): Process_Result = {
- progress.bash(
- Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
- env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
+ ssh.execute(
+ Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
+ "cd " + ssh.bash_path(isabelle_home) + "\n" + script,
+ progress_stdout = progress.echo_if(echo, _),
+ progress_stderr = progress.echo_if(echo, _),
+ redirect = redirect,
+ settings = false,
+ strict = strict)
}
def getenv(name: String): String =
@@ -57,27 +71,52 @@
def etc_settings: Path = etc + Path.explode("settings")
def etc_preferences: Path = etc + Path.explode("preferences")
- def resolve_components(echo: Boolean = false): Unit = {
+
+ /* components */
+
+ def init_components(
+ component_repository: String = Components.default_component_repository,
+ components_base: String = Components.standard_components_base,
+ catalogs: List[String] = Components.default_catalogs,
+ components: List[String] = Nil
+ ): List[String] = {
+ val admin = Components.admin(Path.ISABELLE_HOME).implode
+
+ ("ISABELLE_COMPONENT_REPOSITORY=" + Bash.string(component_repository)) ::
+ catalogs.map(name =>
+ "init_components " + quote(components_base) + " " + quote(admin + "/" + name)) :::
+ components.map(name =>
+ "init_component " + quote(components_base) + "/" + name)
+ }
+
+ 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,
+ clean_platforms = clean_platforms,
+ clean_archives = clean_archives,
+ ssh = ssh,
progress = if (echo) progress else new Progress)
}
}
def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = {
- if (fresh) {
- Isabelle_System.rm_tree(isabelle_home + Path.explode("lib/classes"))
- }
+ if (fresh) ssh.rm_tree(isabelle_home + Path.explode("lib/classes"))
val dummy_stty = Path.explode("~~/lib/dummy_stty/stty")
- if (!expand_path(dummy_stty).is_file) {
- Isabelle_System.copy_file(dummy_stty,
- Isabelle_System.make_directory(expand_path(dummy_stty.dir)))
+ val dummy_stty_remote = expand_path(dummy_stty)
+ if (!ssh.is_file(dummy_stty_remote)) {
+ ssh.make_directory(dummy_stty_remote.dir)
+ ssh.write_file(dummy_stty_remote, dummy_stty)
+ ssh.set_executable(dummy_stty_remote, true)
}
try {
bash(
- "export PATH=\"" + bash_path(dummy_stty.dir) + ":$PATH\"\n" +
+ "export PATH=\"" + bash_path(dummy_stty_remote.dir) + ":$PATH\"\n" +
"export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" +
"bin/isabelle jedit -b", echo = echo).check
}
@@ -85,36 +124,20 @@
}
- /* components */
-
- def init_components(
- component_repository: String = Components.default_component_repository,
- catalogs: List[String] = Components.default_catalogs,
- components: List[String] = Nil
- ): List[String] = {
- val admin = Components.admin(Path.ISABELLE_HOME).implode
- val components_base = quote("${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}")
-
- ("ISABELLE_COMPONENT_REPOSITORY=" + Bash.string(component_repository)) ::
- catalogs.map(name => "init_components " + components_base + " " + quote(admin + "/" + name)) :::
- components.map(name => "init_component " + components_base + "/" + name)
- }
-
-
/* settings */
def clean_settings(): Boolean =
- if (!etc_settings.is_file) true
- else if (File.read(etc_settings).startsWith("# generated by Isabelle")) {
- etc_settings.file.delete
+ if (!ssh.is_file(etc_settings)) true
+ else if (ssh.read(etc_settings).startsWith("# generated by Isabelle")) {
+ ssh.delete(etc_settings)
true
}
else false
def init_settings(settings: List[String]): Unit = {
if (clean_settings()) {
- Isabelle_System.make_directory(etc_settings.dir)
- File.write(etc_settings,
+ ssh.make_directory(etc_settings.dir)
+ ssh.write(etc_settings,
"# generated by Isabelle " + Date.now() + "\n" +
"#-*- shell-script -*- :mode=shellscript:\n" +
settings.mkString("\n", "\n", "\n"))
@@ -123,11 +146,27 @@
}
+ def init(
+ other_settings: List[String] = init_components(),
+ fresh: 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,
+ clean_platforms = clean_platforms,
+ clean_archives = clean_archives)
+ scala_build(fresh = fresh, echo = echo)
+ }
+
+
/* cleanup */
def cleanup(): Unit = {
clean_settings()
- etc.file.delete
- isabelle_home_user.file.delete
+ ssh.delete(etc)
+ ssh.delete(isabelle_home_user)
}
}
--- a/src/Pure/General/ssh.scala Wed Jan 25 13:37:44 2023 +0000
+++ b/src/Pure/General/ssh.scala Wed Jan 25 22:00:21 2023 +0100
@@ -120,6 +120,7 @@
opts: String = "",
args: String = "",
cwd: JFile = null,
+ redirect: Boolean = false,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
strict: Boolean = true
@@ -131,8 +132,11 @@
Config.command(command, config) +
(if (opts.nonEmpty) " " + opts else "") +
(if (args.nonEmpty) " -- " + args else "")
- Isabelle_System.bash(cmd, cwd = cwd, progress_stdout = progress_stdout,
- progress_stderr = progress_stderr, strict = strict)
+ Isabelle_System.bash(cmd, cwd = cwd,
+ redirect = redirect,
+ progress_stdout = progress_stdout,
+ progress_stderr = progress_stderr,
+ strict = strict)
}
def run_sftp(
@@ -183,6 +187,7 @@
override def execute(cmd_line: String,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
+ redirect: Boolean = false,
settings: Boolean = true,
strict: Boolean = true
): Process_Result = {
@@ -190,6 +195,7 @@
args = Bash.string(host) + " " + Bash.string(cmd_line),
progress_stdout = progress_stdout,
progress_stderr = progress_stderr,
+ redirect = redirect,
strict = strict)
}
@@ -222,11 +228,19 @@
override def bash_path(path: Path): String = Bash.string(remote_path(path))
def sftp_path(path: Path): String = sftp_string(remote_path(path))
- def rm(path: Path): Unit = run_sftp("rm " + sftp_path(path))
-
override def is_dir(path: Path): Boolean = run_ssh(args = "test -d " + bash_path(path)).ok
override def is_file(path: Path): Boolean = run_ssh(args = "test -f " + bash_path(path)).ok
+ override def delete(path: Path): Unit = {
+ val cmd = if (is_dir(path)) "rmdir" else if (is_file(path)) "rm" else ""
+ if (cmd.nonEmpty) run_sftp(cmd + " " + sftp_path(path))
+ }
+
+ override def set_executable(path: Path, flag: Boolean): Unit =
+ if (!execute("chmod a" + (if (flag) "+" else "-") + "x " + bash_path(path)).ok) {
+ error("Failed to change executable status of " + quote(remote_path(path)))
+ }
+
override def make_directory(path: Path): Path = {
if (!execute("mkdir -p " + bash_path(path)).ok) {
error("Failed to create directory: " + quote(remote_path(path)))
@@ -242,7 +256,7 @@
}
}
- def read_dir(path: Path): List[String] =
+ override def read_dir(path: Path): List[String] =
run_sftp("@cd " + sftp_path(path) + "\n@ls -1 -a").out_lines.flatMap(s =>
if (s == "." || s == "..") None
else Some(Library.perhaps_unprefix("./", s)))
@@ -267,15 +281,15 @@
override def write_file(path: Path, local_path: Path): Unit =
put_file(path, Isabelle_System.copy_file(local_path, _))
- def write_bytes(path: Path, bytes: Bytes): Unit =
+ override def write_bytes(path: Path, bytes: Bytes): Unit =
put_file(path, Bytes.write(_, bytes))
- def write(path: Path, text: String): Unit =
+ override def write(path: Path, text: String): Unit =
put_file(path, File.write(_, text))
/* tmp dirs */
- def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
+ override def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
def rm_tree(remote_dir: String): Unit =
execute("rm -r -f " + Bash.string(remote_dir)).check
@@ -367,22 +381,30 @@
def bash_path(path: Path): String = File.bash_path(path)
def is_dir(path: Path): Boolean = path.is_dir
def is_file(path: Path): Boolean = path.is_file
+ def delete(path: Path): Unit = path.file.delete
+ def set_executable(path: Path, flag: Boolean): Unit = File.set_executable(path, flag)
def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
+ def rm_tree(dir: Path): Unit = Isabelle_System.rm_tree(dir)
def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
+ def read_dir(path: Path): List[String] = File.read_dir(path)
def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
- def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
def read_bytes(path: Path): Bytes = Bytes.read(path)
def read(path: Path): String = File.read(path)
+ def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
+ def write_bytes(path: Path, bytes: Bytes): Unit = Bytes.write(path, bytes)
+ def write(path: Path, text: String): Unit = File.write(path, text)
def execute(command: String,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
+ redirect: Boolean = false,
settings: Boolean = true,
strict: Boolean = true): Process_Result =
Isabelle_System.bash(command,
progress_stdout = progress_stdout,
progress_stderr = progress_stderr,
+ redirect = redirect,
env = if (settings) Isabelle_System.settings() else null,
strict = strict)
--- a/src/Pure/System/components.scala Wed Jan 25 13:37:44 2023 +0000
+++ b/src/Pure/System/components.scala Wed Jan 25 22:00:21 2023 +0100
@@ -33,12 +33,37 @@
}
+ /* 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 =
Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY")
val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
+ val standard_components_base: String = "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}"
val default_catalogs: List[String] = List("main")
val optional_catalogs: List[String] = List("main", "optional")
@@ -55,7 +80,7 @@
progress: Progress = new Progress
): String = {
val name = Archive.get_name(archive.file_name)
- progress.echo("Unpacking " + name)
+ progress.echo("Unpacking " + archive.base)
ssh.execute(
"tar -C " + ssh.bash_path(dir) + " -x -z -f " + ssh.bash_path(archive),
progress_stdout = progress.echo,
@@ -63,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)
+ }
}
@@ -112,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 */