# HG changeset patch # User wenzelm # Date 1620326592 -7200 # Node ID c88faa1e09e1f47a405357bc134320a1febe5e16 # Parent 7e465e166bb2c839659614fdb79bddeaaabe3061 support local build_heaps; more robust build_release; diff -r 7e465e166bb2 -r c88faa1e09e1 src/Pure/Admin/build_release.scala --- 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 } diff -r 7e465e166bb2 -r c88faa1e09e1 src/Pure/General/ssh.scala --- 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() }