--- 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)
+ }
}
}
--- 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) }
--- 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))
}
--- 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)
}
}
--- 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)
- }
-}