# HG changeset patch # User wenzelm # Date 1476634939 -7200 # Node ID fb3bc899fd513c0e336fcaf4c86698e1c5b2a079 # Parent 15d1ee6e847beeccf9133eaab206e0aeeb9421d6# Parent 5389ebfd576db24518f570ba31cd4ede17778435 merged diff -r 15d1ee6e847b -r fb3bc899fd51 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Sun Oct 16 09:31:06 2016 +0200 +++ b/src/Pure/Admin/build_history.scala Sun Oct 16 18:22:19 2016 +0200 @@ -194,7 +194,7 @@ other_isabelle.isabelle_home_user + Build_Log.log_subdir(build_history_date) + Build_Log.log_filename( - BUILD_HISTORY, build_history_date, build_host, ml_platform, "M" + threads).ext("gz") + BUILD_HISTORY, build_history_date, build_host, ml_platform, "M" + threads) val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info() @@ -226,11 +226,11 @@ }) Isabelle_System.mkdirs(log_path.dir) - File.write_gzip(log_path, + File.write_xz(log_path.ext("xz"), terminate_lines( Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines ::: ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) ::: - heap_sizes)) + heap_sizes), XZ.options(6)) /* next build */ @@ -238,6 +238,8 @@ if (multicore_base && first_build && isabelle_output_log.is_dir) Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log) + Isabelle_System.rm_tree(isabelle_output) + first_build = false (res, log_path) @@ -331,7 +333,7 @@ /** remote build_history -- via command-line **/ def remote_build_history( - session: SSH.Session, + ssh: SSH.Session, isabelle_repos_self: Path, isabelle_repos_other: Path, isabelle_repos_source: String = "http://isabelle.in.tum.de/repos/isabelle", @@ -340,37 +342,37 @@ options: String = "", args: String = ""): List[(String, Bytes)] = { - using(session.sftp())(sftp => - { - val isabelle_admin = sftp.remote_path(isabelle_repos_self + Path.explode("Admin")) + val isabelle_admin = ssh.remote_path(isabelle_repos_self + Path.explode("Admin")) - /* prepare repository clones */ + /* prepare repository clones */ - val isabelle_hg = - Mercurial.setup_repository( - isabelle_repos_source, isabelle_repos_self, ssh = Some(session)) + val isabelle_hg = + Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = Some(ssh)) - if (self_update) { - isabelle_hg.pull() - isabelle_hg.update(clean = true) - session.execute(File.bash_string(isabelle_admin + "/build") + " jars_fresh").check - } + if (self_update) { + isabelle_hg.pull() + isabelle_hg.update(clean = true) + ssh.execute(File.bash_string(isabelle_admin + "/build") + " jars_fresh").check + } - Mercurial.setup_repository( - sftp.remote_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(session)) + Mercurial.setup_repository( + ssh.remote_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh)) - /* Admin/build_history */ + /* Admin/build_history */ - val result = - session.execute( - File.bash_string(isabelle_admin + "/build_history") + " " + options + " " + - File.bash_string(sftp.remote_path(isabelle_repos_other)) + " " + args, - progress_stderr = progress.echo(_)).check + val result = + ssh.execute( + File.bash_string(isabelle_admin + "/build_history") + " " + options + " " + + File.bash_string(ssh.remote_path(isabelle_repos_other)) + " " + args, + progress_stderr = progress.echo(_)).check - for (line <- result.out_lines; log = Path.explode(line)) - yield (log.base.implode, sftp.read_bytes(log)) - }) + for (line <- result.out_lines; log = Path.explode(line)) + yield { + val bytes = ssh.read_bytes(log) + ssh.rm(log) + (log.base.implode, bytes) + } } } diff -r 15d1ee6e847b -r fb3bc899fd51 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Sun Oct 16 09:31:06 2016 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Oct 16 18:22:19 2016 +0200 @@ -40,12 +40,7 @@ Logger_Task("isabelle_identify", logger => { val isabelle_id = Mercurial.repository(isabelle_repos).id() - val afp_id = - { - val hg = Mercurial.setup_repository(afp_source, afp_repos) - hg.pull() - hg.id() - } + val afp_id = Mercurial.setup_repository(afp_source, afp_repos).id() File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date), terminate_lines( @@ -61,10 +56,13 @@ private val build_history_base = Logger_Task("build_history_base", logger => { + val hg = + Mercurial.setup_repository( + File.standard_path(isabelle_repos), isabelle_repos_test) for { (result, log_path) <- - Build_History.build_history(Mercurial.repository(isabelle_repos_test), - rev = "build_history_base", fresh = true, build_args = List("HOL")) + Build_History.build_history( + hg, rev = "build_history_base", fresh = true, build_args = List("HOL")) } { result.check File.copy(log_path, logger.log_dir + log_path.base) @@ -112,10 +110,10 @@ Logger_Task("build_history-" + r.host, logger => { using(logger.ssh_context.open_session(host = r.host, user = r.user, port = r.port))( - session => + ssh => { val results = - Build_History.remote_build_history(session, + Build_History.remote_build_history(ssh, isabelle_repos, isabelle_repos.ext(r.host), isabelle_repos_source = isabelle_dev_source, @@ -133,7 +131,7 @@ sealed case class Logger_Task(name: String = "", body: Logger => Unit) - class Log_Service private[Isabelle_Cronjob](progress: Progress, val ssh_context: SSH) + class Log_Service private[Isabelle_Cronjob](progress: Progress, val ssh_context: SSH.Context) { current_log.file.delete @@ -179,7 +177,7 @@ class Logger private[Isabelle_Cronjob]( val log_service: Log_Service, val start_date: Date, val task_name: String) { - def ssh_context: SSH = log_service.ssh_context + def ssh_context: SSH.Context = log_service.ssh_context def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg) @@ -225,7 +223,7 @@ /* log service */ - val log_service = new Log_Service(progress, SSH.init(Options.init())) + val log_service = new Log_Service(progress, SSH.init_context(Options.init())) def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) } diff -r 15d1ee6e847b -r fb3bc899fd51 src/Pure/Admin/remote_dmg.scala --- a/src/Pure/Admin/remote_dmg.scala Sun Oct 16 09:31:06 2016 +0200 +++ b/src/Pure/Admin/remote_dmg.scala Sun Oct 16 18:22:19 2016 +0200 @@ -9,21 +9,20 @@ object Remote_DMG { - def remote_dmg(session: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "") + def remote_dmg(ssh: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "") { - session.with_tmp_dir(remote_dir => - using(session.sftp())(sftp => - { - val cd = "cd " + File.bash_string(sftp.remote_path(remote_dir)) + "; " + ssh.with_tmp_dir(remote_dir => + { + val cd = "cd " + File.bash_string(ssh.remote_path(remote_dir)) + "; " - sftp.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file) - session.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check - session.execute( - cd + "hdiutil create -srcfolder root" + - (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) + - " dmg.dmg").check - sftp.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file) - })) + ssh.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file) + ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check + ssh.execute( + cd + "hdiutil create -srcfolder root" + + (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) + + " dmg.dmg").check + ssh.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file) + }) } @@ -57,7 +56,7 @@ case _ => getopts.usage() } - val ssh = SSH.init(Options.init) + val ssh = SSH.init_context(Options.init) using(ssh.open_session(user = user, host = host, port = port))( remote_dmg(_, tar_gz_file, dmg_file, volume_name)) } diff -r 15d1ee6e847b -r fb3bc899fd51 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Sun Oct 16 09:31:06 2016 +0200 +++ b/src/Pure/General/mercurial.scala Sun Oct 16 18:22:19 2016 +0200 @@ -35,18 +35,24 @@ source: String, root: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository = { val hg = new Repository(root, ssh) + ssh match { + case None => Isabelle_System.mkdirs(hg.root.dir) + case Some(ssh) => ssh.mkdirs(hg.root.dir) + } hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check hg } def setup_repository(source: String, root: Path, ssh: Option[SSH.Session] = None): Repository = - ssh match { - case None => if (root.is_dir) repository(root) else clone_repository(source, root) - case Some(session) => - using(session.sftp())(sftp => - if (sftp.is_dir(root)) repository(root, ssh = ssh) - else clone_repository(source, root, ssh = ssh)) - } + { + val present = + ssh match { + case None => root.is_dir + case Some(ssh) => ssh.is_dir(root) + } + if (present) { val hg = repository(root, ssh = ssh); hg.pull(); hg } + else clone_repository(source, root, options = "--noupdate", ssh = ssh) + } class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session]) { @@ -55,13 +61,13 @@ val root = ssh match { case None => root_path.expand - case Some(session) => using(session.sftp())(sftp => root_path.expand_env(sftp.settings)) + case Some(ssh) => root_path.expand_env(ssh.settings) } override def toString: String = ssh match { case None => root.implode - case Some(session) => session.toString + ":" + root.implode + case Some(ssh) => ssh.toString + ":" + root.implode } def command(name: String, args: String = "", options: String = ""): Process_Result = @@ -72,7 +78,7 @@ " --noninteractive " + name + " " + options + " " + args ssh match { case None => Isabelle_System.bash(cmdline) - case Some(session) => session.execute(cmdline) + case Some(ssh) => ssh.execute(cmdline) } } diff -r 15d1ee6e847b -r fb3bc899fd51 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Sun Oct 16 09:31:06 2016 +0200 +++ b/src/Pure/General/ssh.scala Sun Oct 16 18:22:19 2016 +0200 @@ -38,10 +38,13 @@ val default_port = 22 + def connect_timeout(options: Options): Int = + options.seconds("ssh_connect_timeout").ms.toInt - /* init */ - def init(options: Options): SSH = + /* init context */ + + def init_context(options: Options): Context = { val config_dir = Path.explode(options.string("ssh_config_dir")) if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir) @@ -61,11 +64,30 @@ for (identity_file <- identity_files if identity_file.is_file) jsch.addIdentity(File.platform_path(identity_file)) - new SSH(options, jsch) + new Context(options, jsch) } - def connect_timeout(options: Options): Int = - options.seconds("ssh_connect_timeout").ms.toInt + class Context private[SSH](val options: Options, val jsch: JSch) + { + def update_options(new_options: Options): Context = new Context(new_options, jsch) + + def open_session(host: String, user: String = "", port: Int = default_port): Session = + { + val session = jsch.getSession(if (user == "") null else user, host, port) + + session.setUserInfo(No_User_Info) + session.setConfig("MaxAuthTries", "3") + + if (options.bool("ssh_compression")) { + session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none") + session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none") + session.setConfig("compression_level", "9") + } + + session.connect(connect_timeout(options)) + new Session(options, session) + } + } /* logging */ @@ -103,17 +125,6 @@ } - /* channel */ - - class Channel[C <: JSch_Channel] private[SSH]( - val session: Session, val kind: String, val channel: C) - { - override def toString: String = kind + " " + session.toString - - def close() { channel.disconnect } - } - - /* Sftp channel */ type Attrs = SftpATTRS @@ -124,82 +135,16 @@ def is_dir: Boolean = attrs.isDir } - class Sftp private[SSH](session: Session, kind: String, channel: ChannelSftp) - extends Channel[ChannelSftp](session, kind, channel) - { - channel.connect(connect_timeout(session.options)) - - val settings: Map[String, String] = - { - val home = channel.getHome - Map("HOME" -> home, "USER_HOME" -> home) - } - def expand_path(path: Path): Path = path.expand_env(settings) - def remote_path(path: Path): String = expand_path(path).implode - - def chmod(permissions: Int, path: Path): Unit = channel.chmod(permissions, remote_path(path)) - def mv(path1: Path, path2: Path): Unit = channel.rename(remote_path(path1), remote_path(path2)) - def rm(path: Path): Unit = channel.rm(remote_path(path)) - def mkdir(path: Path): Unit = channel.mkdir(remote_path(path)) - def rmdir(path: Path): Unit = channel.rmdir(remote_path(path)) - - def stat(path: Path): Option[Dir_Entry] = - try { Some(Dir_Entry(expand_path(path), channel.stat(remote_path(path)))) } - catch { case _: SftpException => None } - - def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false - def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false - - def read_dir(path: Path): List[Dir_Entry] = - { - val dir = channel.ls(remote_path(path)) - (for { - i <- (0 until dir.size).iterator - a = dir.get(i).asInstanceOf[AnyRef] - name = Untyped.get[String](a, "filename") - attrs = Untyped.get[Attrs](a, "attrs") - if name != "." && name != ".." - } yield Dir_Entry(Path.basic(name), attrs)).toList - } - - def find_files(root: Path, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] = - { - def find(dir: Path): List[Dir_Entry] = - read_dir(dir).flatMap(entry => - { - val file = dir + entry.name - if (entry.is_dir) find(file) - else if (pred(entry)) List(entry.copy(name = file)) - else Nil - }) - find(root) - } - - def open_input(path: Path): InputStream = channel.get(remote_path(path)) - def open_output(path: Path): OutputStream = channel.put(remote_path(path)) - - def read_file(path: Path, local_path: Path): Unit = - channel.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 = - channel.put(File.platform_path(local_path), remote_path(path)) - def write_bytes(path: Path, bytes: Bytes): Unit = - using(open_output(path))(bytes.write_stream(_)) - def write(path: Path, text: String): Unit = - using(open_output(path))(stream => Bytes(text).write_stream(stream)) - } - /* exec channel */ private val exec_wait_delay = Time.seconds(0.3) - class Exec private[SSH](session: Session, kind: String, channel: ChannelExec) - extends Channel[ChannelExec](session, kind, channel) + class Exec private[SSH](session: Session, channel: ChannelExec) { - def kill(signal: String) { channel.sendSignal(signal) } + override def toString: String = "exec " + session.toString + + def close() { channel.disconnect } val exit_status: Future[Int] = Future.thread("ssh_wait") { @@ -283,21 +228,90 @@ (if (session.getPort == default_port) "" else ":" + session.getPort) + (if (session.isConnected) "" else " (disconnected)") - def close() { session.disconnect } + + /* sftp channel */ + + val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp] + sftp.connect(connect_timeout(options)) + + def close() { sftp.disconnect; session.disconnect } + + val settings: Map[String, String] = + { + val home = sftp.getHome + Map("HOME" -> home, "USER_HOME" -> home) + } + def expand_path(path: Path): Path = path.expand_env(settings) + def remote_path(path: Path): String = expand_path(path).implode - def sftp(): Sftp = + def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path)) + def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2)) + def rm(path: Path): Unit = sftp.rm(remote_path(path)) + def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path)) + def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path)) + + def stat(path: Path): Option[Dir_Entry] = + try { Some(Dir_Entry(expand_path(path), sftp.stat(remote_path(path)))) } + catch { case _: SftpException => None } + + def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false + def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false + + def mkdirs(path: Path): Unit = + if (!is_dir(path)) { + execute( + "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"") + if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path))) + } + + def read_dir(path: Path): List[Dir_Entry] = { - val kind = "sftp" - val channel = session.openChannel(kind).asInstanceOf[ChannelSftp] - new Sftp(this, kind, channel) + val dir = sftp.ls(remote_path(path)) + (for { + i <- (0 until dir.size).iterator + a = dir.get(i).asInstanceOf[AnyRef] + name = Untyped.get[String](a, "filename") + attrs = Untyped.get[Attrs](a, "attrs") + if name != "." && name != ".." + } yield Dir_Entry(Path.basic(name), attrs)).toList } + def find_files(root: Path, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] = + { + def find(dir: Path): List[Dir_Entry] = + read_dir(dir).flatMap(entry => + { + val file = dir + entry.name + if (entry.is_dir) find(file) + else if (pred(entry)) List(entry.copy(name = file)) + else Nil + }) + find(root) + } + + 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 = + 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 = + 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(_)) + def write(path: Path, text: String): Unit = + using(open_output(path))(stream => Bytes(text).write_stream(stream)) + + + /* exec channel */ + def exec(command: String): Exec = { - val kind = "exec" - val channel = session.openChannel(kind).asInstanceOf[ChannelExec] + val channel = session.openChannel("exec").asInstanceOf[ChannelExec] channel.setCommand("export USER_HOME=\"$HOME\"\n" + command) - new Exec(this, kind, channel) + new Exec(this, channel) } def execute(command: String, @@ -322,25 +336,3 @@ } } } - -class SSH private(val options: Options, val jsch: JSch) -{ - def update_options(new_options: Options): SSH = new SSH(new_options, jsch) - - def open_session(host: String, user: String = "", port: Int = SSH.default_port): SSH.Session = - { - val session = jsch.getSession(if (user == "") null else user, host, port) - - session.setUserInfo(SSH.No_User_Info) - session.setConfig("MaxAuthTries", "3") - - if (options.bool("ssh_compression")) { - session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none") - session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none") - session.setConfig("compression_level", "9") - } - - session.connect(SSH.connect_timeout(options)) - new SSH.Session(options, session) - } -}