--- a/src/Pure/Admin/build_release.scala Wed May 05 21:14:38 2021 +0200
+++ b/src/Pure/Admin/build_release.scala Thu May 06 20:43:12 2021 +0200
@@ -223,39 +223,45 @@
/** build release **/
- /* build heaps on remote server */
+ /* build heaps */
- private def remote_build_heaps(
+ private def build_heaps(
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
local_dir: Path): Unit =
{
val server_option = "build_host_" + platform.toString
- options.string(server_option) match {
- case SSH.Target(user, host) =>
- using(SSH.open_session(options, host = host, user = user))(ssh =>
- Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar =>
- {
- execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
- ssh.with_tmp_dir(remote_dir =>
- {
- val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
- ssh.write_file(remote_tmp_tar, local_tmp_tar)
- val remote_commands =
- List(
- "cd " + File.bash_path(remote_dir),
- "tar -xf tmp.tar",
- "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
- "tar -cf tmp.tar heaps")
- ssh.execute(remote_commands.mkString(" && ")).check
- ssh.read_file(remote_tmp_tar, local_tmp_tar)
- })
- execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
- })
- )
- case s => error("Bad " + server_option + ": " + quote(s))
+ val ssh =
+ options.string(server_option) match {
+ case "" =>
+ if (Platform.family == platform) SSH.Local
+ else error("Undefined option " + server_option + ": cannot build heaps")
+ case SSH.Target(user, host) =>
+ SSH.open_session(options, host = host, user = user)
+ case s => error("Malformed option " + server_option + ": " + quote(s))
+ }
+ try {
+ Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar =>
+ {
+ execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
+ ssh.with_tmp_dir(remote_dir =>
+ {
+ val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
+ ssh.write_file(remote_tmp_tar, local_tmp_tar)
+ val remote_commands =
+ List(
+ "cd " + File.bash_path(remote_dir),
+ "tar -xf tmp.tar",
+ "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
+ "tar -cf tmp.tar heaps")
+ ssh.execute(remote_commands.mkString(" && "), settings = false).check
+ ssh.read_file(remote_tmp_tar, local_tmp_tar)
+ })
+ execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
+ })
}
+ finally { ssh.close() }
}
@@ -594,8 +600,8 @@
// build heaps
if (build_sessions.nonEmpty) {
- progress.echo("Building heaps ...")
- remote_build_heaps(options, platform, build_sessions, isabelle_target)
+ progress.echo("Building heaps " + commas_quote(build_sessions) + " ...")
+ build_heaps(options, platform, build_sessions, isabelle_target)
}
@@ -901,11 +907,12 @@
if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
error("Building for windows requires 7z")
+ val progress = new Console_Progress()
def make_context(name: String): Release_Context =
Release_Context(target_dir,
release_name = name,
components_base = components_base,
- progress = new Console_Progress())
+ progress = progress)
val context =
if (source_archive.isEmpty) {
@@ -915,9 +922,10 @@
context
}
else {
- val archive = Release_Archive.get(source_archive, rename = release_name)
+ val archive =
+ Release_Archive.get(source_archive, rename = release_name, progress = progress)
val context = make_context(archive.identifier)
- Isabelle_System.new_directory(context.dist_dir)
+ Isabelle_System.make_directory(context.dist_dir)
use_release_archive(context, archive, id = rev)
context
}
--- a/src/Pure/General/ssh.scala Wed May 05 21:14:38 2021 +0200
+++ b/src/Pure/General/ssh.scala Thu May 06 20:43:12 2021 +0200
@@ -318,7 +318,7 @@
val session: JSch_Session,
on_close: () => Unit,
val nominal_host: String,
- val nominal_user: String) extends System with AutoCloseable
+ val nominal_user: String) extends System
{
def update_options(new_options: Options): Session =
new Session(new_options, session, on_close, nominal_host, nominal_user)
@@ -347,7 +347,7 @@
val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
sftp.connect(connect_timeout(options))
- def close(): Unit = { sftp.disconnect; session.disconnect; on_close() }
+ override def close(): Unit = { sftp.disconnect; session.disconnect; on_close() }
val settings: Map[String, String] =
{
@@ -438,12 +438,12 @@
def open_input(path: Path): InputStream = sftp.get(remote_path(path))
def open_output(path: Path): OutputStream = sftp.put(remote_path(path))
- def read_file(path: Path, local_path: Path): Unit =
+ override def read_file(path: Path, local_path: Path): Unit =
sftp.get(remote_path(path), File.platform_path(local_path))
def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
def read(path: Path): String = using(open_input(path))(File.read_stream)
- def write_file(path: Path, local_path: Path): Unit =
+ override def write_file(path: Path, local_path: Path): Unit =
sftp.put(File.platform_path(local_path), remote_path(path))
def write_bytes(path: Path, bytes: Bytes): Unit =
using(open_output(path))(bytes.write_stream)
@@ -463,6 +463,7 @@
override def execute(command: String,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
+ settings: Boolean = true,
strict: Boolean = true): Process_Result =
exec(command).result(progress_stdout, progress_stderr, strict)
@@ -479,7 +480,7 @@
def tmp_dir(): String =
execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
- def with_tmp_dir[A](body: Path => A): A =
+ override def with_tmp_dir[A](body: Path => A): A =
{
val remote_dir = tmp_dir()
try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
@@ -489,8 +490,10 @@
/* system operations */
- trait System
+ trait System extends AutoCloseable
{
+ def close(): Unit = ()
+
def hg_url: String = ""
def expand_path(path: Path): Path = path.expand
@@ -498,13 +501,20 @@
def is_dir(path: Path): Boolean = path.is_dir
def is_file(path: Path): Boolean = path.is_file
def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
+ def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
+ 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 execute(command: String,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
+ settings: Boolean = true,
strict: Boolean = true): Process_Result =
- Isabelle_System.bash(command, progress_stdout = progress_stdout,
- progress_stderr = progress_stderr, strict = strict)
+ Isabelle_System.bash(command,
+ progress_stdout = progress_stdout,
+ progress_stderr = progress_stderr,
+ env = if (settings) Isabelle_System.settings() else null,
+ strict = strict)
def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
}