--- a/src/Doc/System/Misc.thy Tue Sep 13 10:44:47 2022 +0200
+++ b/src/Doc/System/Misc.thy Tue Sep 13 11:56:38 2022 +0200
@@ -315,10 +315,11 @@
-P protect spaces in target file names: more robust, less portable
-R ROOT explicit repository root directory
(default: implicit from current directory)
+ -S PATH SSH control path for connection multiplexing
-T thorough treatment of file content and directory times
-n no changes: dry-run
+ -p PORT SSH port
-r REV explicit revision (default: state of working directory)
- -p PORT explicit SSH port
-v verbose
Synchronize Mercurial repository with TARGET directory,
@@ -355,6 +356,9 @@
\<^medskip> Option \<^verbatim>\<open>-p\<close> specifies an explicit port for the SSH connection underlying
\<^verbatim>\<open>rsync\<close>; the default is taken from the user's \<^path>\<open>ssh_config\<close> file.
+ \<^medskip> Option \<^verbatim>\<open>-S\<close> specifies the control path (Unix socket) to an existing SSH
+ connection that supports multiplexing (\<^verbatim>\<open>ssh -M -S\<close>~\<open>socket\<close>).
+
\<^medskip> Option \<^verbatim>\<open>-P\<close> uses \<^verbatim>\<open>rsync --protect-args\<close> to work robustly with spaces or
special characters of the shell. This requires at least \<^verbatim>\<open>rsync 3.0.0\<close>,
which is not always available --- notably on macOS. Assuming traditional
--- a/src/Doc/System/Sessions.thy Tue Sep 13 10:44:47 2022 +0200
+++ b/src/Doc/System/Sessions.thy Tue Sep 13 11:56:38 2022 +0200
@@ -932,11 +932,12 @@
(based on accidental local state)
-J preserve *.jar files
-P protect spaces in target file names: more robust, less portable
+ -S PATH SSH control path for connection multiplexing
-T thorough treatment of file content and directory times
-a REV explicit AFP revision (default: state of working directory)
-n no changes: dry-run
+ -p PORT SSH port
-r REV explicit revision (default: state of working directory)
- -p PORT explicit SSH port
-v verbose
Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".\<close>}
@@ -950,8 +951,8 @@
sub-directory with the literal name \<^verbatim>\<open>AFP\<close>; thus it can be easily included
elsewhere, e.g. @{tool build}~\<^verbatim>\<open>-d\<close>~\<^verbatim>\<open>'~~/AFP'\<close> on the remote side.
- \<^medskip> Options \<^verbatim>\<open>-P\<close>, \<^verbatim>\<open>-T\<close>, \<^verbatim>\<open>-n\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-v\<close> are the same as the underlying
- @{tool hg_sync}.
+ \<^medskip> Options \<^verbatim>\<open>-P\<close>, \<^verbatim>\<open>-S\<close>, \<^verbatim>\<open>-T\<close>, \<^verbatim>\<open>-n\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-v\<close> are the same as the
+ underlying @{tool hg_sync}.
\<^medskip> Options \<^verbatim>\<open>-r\<close> and \<^verbatim>\<open>-a\<close> are the same as option \<^verbatim>\<open>-r\<close> for @{tool hg_sync},
but for the Isabelle and AFP repositories, respectively. The AFP version is
--- a/src/Pure/Admin/build_history.scala Tue Sep 13 10:44:47 2022 +0200
+++ b/src/Pure/Admin/build_history.scala Tue Sep 13 11:56:38 2022 +0200
@@ -535,7 +535,9 @@
def sync(target: Path, accurate: Boolean = false,
rev: String = "", afp_rev: String = "", afp: Boolean = false
): Unit = {
- val context = Rsync.Context(progress, port = ssh.port, protect_args = protect_args)
+ val context =
+ Rsync.Context(progress, ssh_port = ssh.port, ssh_control_path = ssh.control_path,
+ protect_args = protect_args)
Sync.sync(ssh.options, context, ssh.rsync_path(target),
thorough = accurate, preserve_jars = !accurate,
rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)
--- a/src/Pure/General/mercurial.scala Tue Sep 13 10:44:47 2022 +0200
+++ b/src/Pure/General/mercurial.scala Tue Sep 13 11:56:38 2022 +0200
@@ -563,10 +563,11 @@
var filter: List[String] = Nil
var protect_args = false
var root: Option[Path] = None
+ var ssh_control_path = ""
var thorough = false
var dry_run = false
+ var ssh_port = 0
var rev = ""
- var port = 0
var verbose = false
val getopts = Getopts("""
@@ -578,10 +579,11 @@
-P protect spaces in target file names: more robust, less portable
-R ROOT explicit repository root directory
(default: implicit from current directory)
+ -S PATH SSH control path for connection multiplexing
-T thorough treatment of file content and directory times
-n no changes: dry-run
+ -p PORT SSH port
-r REV explicit revision (default: state of working directory)
- -p PORT explicit SSH port
-v verbose
Synchronize Mercurial repository with TARGET directory,
@@ -590,10 +592,11 @@
"F:" -> (arg => filter = filter ::: List(arg)),
"P" -> (_ => protect_args = true),
"R:" -> (arg => root = Some(Path.explode(arg))),
+ "S:" -> (arg => ssh_control_path = arg),
"T" -> (_ => thorough = true),
"n" -> (_ => dry_run = true),
+ "p:" -> (arg => ssh_port = Value.Int.parse(arg)),
"r:" -> (arg => rev = arg),
- "p:" -> (arg => port = Value.Int.parse(arg)),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
@@ -609,7 +612,8 @@
case Some(dir) => repository(dir)
case None => the_repository(Path.current)
}
- val context = Rsync.Context(progress, port = port, protect_args = protect_args)
+ val context = Rsync.Context(progress, ssh_port = ssh_port,
+ ssh_control_path = ssh_control_path, protect_args = protect_args)
hg.sync(context, target, verbose = verbose, thorough = thorough,
dry_run = dry_run, filter = filter, rev = rev)
}
--- a/src/Pure/General/rsync.scala Tue Sep 13 10:44:47 2022 +0200
+++ b/src/Pure/General/rsync.scala Tue Sep 13 11:56:38 2022 +0200
@@ -9,14 +9,23 @@
object Rsync {
sealed case class Context(progress: Progress,
- port: Int = 0,
+ ssh_port: Int = 0,
+ ssh_control_path: String = "",
archive: Boolean = true,
protect_args: Boolean = true // requires rsync 3.0.0, or later
) {
- def command: String =
- "rsync --rsh=" + Bash.string("ssh" + (if (port > 0) "-p " + port else "")) +
+ require(ssh_control_path.isEmpty || ssh_control_path == Bash.string(ssh_control_path),
+ "Malformed socket path: " + quote(ssh_control_path))
+
+ def command: String = {
+ val ssh_command =
+ "ssh" + (if (ssh_port > 0) " -p " + ssh_port else "") +
+ (if (ssh_control_path.nonEmpty) " -o ControlPath=" + ssh_control_path else "")
+
+ "rsync --rsh=" + Bash.string(ssh_command) +
(if (archive) " --archive" else "") +
(if (protect_args) " --protect-args" else "")
+ }
}
def exec(
--- a/src/Pure/General/ssh.scala Tue Sep 13 10:44:47 2022 +0200
+++ b/src/Pure/General/ssh.scala Tue Sep 13 11:56:38 2022 +0200
@@ -98,7 +98,7 @@
val port: Int,
val user: String,
control_master: Boolean,
- control_path: String
+ val control_path: String
) extends System {
ssh =>
--- a/src/Pure/Tools/sync.scala Tue Sep 13 10:44:47 2022 +0200
+++ b/src/Pure/Tools/sync.scala Tue Sep 13 11:56:38 2022 +0200
@@ -88,8 +88,9 @@
var thorough = false
var afp_rev = ""
var dry_run = false
+ var ssh_port = 0
var rev = ""
- var port = 0
+ var ssh_control_path = ""
var verbose = false
val getopts = Getopts("""
@@ -102,11 +103,12 @@
(based on accidental local state)
-J preserve *.jar files
-P protect spaces in target file names: more robust, less portable
+ -S PATH SSH control path for connection multiplexing
-T thorough treatment of file content and directory times
-a REV explicit AFP revision (default: state of working directory)
-n no changes: dry-run
+ -p PORT SSH port
-r REV explicit revision (default: state of working directory)
- -p PORT explicit SSH port
-v verbose
Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".
@@ -116,11 +118,12 @@
"I:" -> (arg => session_images = session_images ::: List(arg)),
"J" -> (_ => preserve_jars = true),
"P" -> (_ => protect_args = true),
+ "S:" -> (arg => ssh_control_path = arg),
"T" -> (_ => thorough = true),
"a:" -> (arg => afp_rev = arg),
"n" -> (_ => dry_run = true),
+ "p:" -> (arg => ssh_port = Value.Int.parse(arg)),
"r:" -> (arg => rev = arg),
- "p:" -> (arg => port = Value.Int.parse(arg)),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
@@ -132,7 +135,9 @@
val options = Options.init()
val progress = new Console_Progress
- val context = Rsync.Context(progress, port = port, protect_args = protect_args)
+ val context =
+ Rsync.Context(progress, ssh_port = ssh_port, ssh_control_path = ssh_control_path,
+ protect_args = protect_args)
sync(options, context, target, verbose = verbose, thorough = thorough,
purge_heaps = purge_heaps, session_images = session_images, preserve_jars = preserve_jars,
dry_run = dry_run, rev = rev, afp_root = afp_root, afp_rev = afp_rev)