# HG changeset patch
# User wenzelm
# Date 1680964674 -7200
# Node ID fb61887c069a1585cf85dcd67bdcd13daf12082f
# Parent  127d077cccfeee993f6bb364b93be3869c680d03
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";

diff -r 127d077cccfe -r fb61887c069a NEWS
--- a/NEWS	Sat Apr 08 10:24:54 2023 +0200
+++ b/NEWS	Sat Apr 08 16:37:54 2023 +0200
@@ -305,6 +305,11 @@
 
 *** System ***
 
+* Remote SSH host of "isabelle hg_sync" and "isabelle sync" now works
+via options -s, -p, -u. The TARGET argument is a plain file-system path
+in Isabelle notation, no longer an rsync target (host:directory). Minor
+INCOMPATIBILITY of command-line syntax.
+
 * System option "build_through" determines if session builds should
 observe dependency of options that contribute to the formal content.
 This is specified via option tags given in etc/options (e.g. see
diff -r 127d077cccfe -r fb61887c069a src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Sat Apr 08 10:24:54 2023 +0200
+++ b/src/Doc/System/Misc.thy	Sat Apr 08 16:37:54 2023 +0200
@@ -323,25 +323,26 @@
     -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
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -p PORT      explicit SSH port
     -r REV       explicit revision (default: state of working directory)
+    -s HOST      SSH host name for remote target (default: local)
+    -u USER      explicit SSH user name
     -v           verbose
 
   Synchronize Mercurial repository with TARGET directory,
-  which can be local or remote (using notation of rsync).\<close>}
+  which can be local or remote (see options -s -p -u).\<close>}
 
-  The \<^verbatim>\<open>TARGET\<close> specification can be a local or remote directory (via ssh),
-  using \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close> notation for
-  destinations; see also examples below. The content is written directly into
-  the target, \<^emph>\<open>without\<close> creating a separate sub-directory. The special
-  sub-directory \<^verbatim>\<open>.hg_sync\<close> within the target contains meta data from the
-  original Mercurial repository. Repeated synchronization is guarded by the
-  presence of a \<^verbatim>\<open>.hg_sync\<close> sub-directory: this sanity check prevents
-  accidental changes (or deletion!) of targets that were not created by @{tool
-  hg_sync}.
+  The \<^verbatim>\<open>TARGET\<close> specifies a directory, which can be local or an a remote SSH
+  host; the latter requires option \<^verbatim>\<open>-s\<close> for the host name. The content is
+  written directly into the target, \<^emph>\<open>without\<close> creating a separate
+  sub-directory. The special sub-directory \<^verbatim>\<open>.hg_sync\<close> within the target
+  contains meta data from the original Mercurial repository. Repeated
+  synchronization is guarded by the presence of a \<^verbatim>\<open>.hg_sync\<close> sub-directory:
+  this sanity check prevents accidental changes (or deletion!) of targets that
+  were not created by @{tool hg_sync}.
 
   \<^medskip> Option \<^verbatim>\<open>-r\<close> specifies an explicit revision of the repository; the default
   is the current state of the working directory (which might be uncommitted).
@@ -361,12 +362,13 @@
   times. The default is to consider files with equal time and size already as
   equal, and to ignore time stamps on directories.
 
+  \<^medskip> Options \<^verbatim>\<open>-s\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-u\<close> specify the SSH connection precisely. If no
+  SSH host name is given, the local file-system is used. An explicit port and
+  user are only required in special situations.
+
   \<^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
@@ -379,7 +381,7 @@
 text \<open>
   Synchronize the current repository onto a remote host, with accurate
   treatment of all content:
-  @{verbatim [display] \<open>  isabelle hg_sync -T remotename:test/repos\<close>}
+  @{verbatim [display] \<open>  isabelle hg_sync -T -s remotename test/repos\<close>}
 \<close>
 
 
diff -r 127d077cccfe -r fb61887c069a src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sat Apr 08 10:24:54 2023 +0200
+++ b/src/Doc/System/Sessions.thy	Sat Apr 08 16:37:54 2023 +0200
@@ -937,11 +937,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)
+    -s HOST      SSH host name for remote target (default: local)
+    -u USER      explicit SSH user name
     -n           no changes: dry-run
-    -p PORT      SSH port
+    -p PORT      explicit SSH port
     -r REV       explicit revision (default: state of working directory)
     -v           verbose
 
@@ -956,8 +957,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>-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>-P\<close>, \<^verbatim>\<open>-T\<close>, \<^verbatim>\<open>-n\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-s\<close>, \<^verbatim>\<open>-u\<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
@@ -1001,7 +1002,7 @@
   For quick testing of Isabelle + AFP on a remote machine, upload changed
   sources, jars, and local sessions images for \<^verbatim>\<open>HOL\<close>:
 
-  @{verbatim [display] \<open>  isabelle sync -A: -I HOL -J testmachine:test/isabelle_afp\<close>}
+  @{verbatim [display] \<open>  isabelle sync -A: -I HOL -J -s testmachine test/isabelle_afp\<close>}
   Assuming that the local \<^verbatim>\<open>HOL\<close> hierarchy has been up-to-date, and the local
   and remote ML platforms coincide, a remote @{tool build} will proceed
   without building \<^verbatim>\<open>HOL\<close> again.
@@ -1010,7 +1011,7 @@
   \<^verbatim>\<open>-J\<close>, but option \<^verbatim>\<open>-T\<close> to disable the default ``quick check'' of \<^verbatim>\<open>rsync\<close>
   (which only inspects file sizes and date stamps); existing heaps are
   deleted:
-  @{verbatim [display] \<open>  isabelle sync -A: -T -H testmachine:test/isabelle_afp\<close>}
+  @{verbatim [display] \<open>  isabelle sync -A: -T -H -s testmachine test/isabelle_afp\<close>}
 \<close>
 
 end
diff -r 127d077cccfe -r fb61887c069a src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Apr 08 10:24:54 2023 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Apr 08 16:37:54 2023 +0200
@@ -548,10 +548,8 @@
     def sync(target: Path, accurate: Boolean = false,
       rev: String = "", afp_rev: String = "", afp: Boolean = false
     ): Unit = {
-      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),
+      val context = Rsync.Context(progress, ssh = ssh, protect_args = protect_args)
+      Sync.sync(ssh.options, context, target,
         thorough = accurate, preserve_jars = !accurate,
         rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)
     }
diff -r 127d077cccfe -r fb61887c069a src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Apr 08 10:24:54 2023 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Apr 08 16:37:54 2023 +0200
@@ -293,7 +293,7 @@
 
     def known_files(): List[String] = status(options = "--modified --added --clean --no-status")
 
-    def sync(context: Rsync.Context, target: String,
+    def sync(context: Rsync.Context, target: Path,
       thorough: Boolean = false,
       dry_run: Boolean = false,
       filter: List[String] = Nil,
@@ -308,10 +308,11 @@
         Rsync.init(context0, target)
 
         val list =
-          Rsync.exec(context0, list = true, args = List("--", Url.direct_path(target)))
+          Rsync.exec(context0, list = true,
+            args = List("--", context.target(target, direct = true)))
             .check.out_lines.filterNot(_.endsWith(" ."))
         if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) {
-          error("No .hg_sync meta data in " + quote(target))
+          error("No .hg_sync meta data in " + quote(context.target(target)))
         }
 
         val id_content = id(rev = rev)
@@ -353,7 +354,7 @@
           prune_empty_dirs = true,
           filter = protect ::: filter,
           args = List("--exclude-from=" + exclude_path.implode, "--",
-            Url.direct_path(source), target)
+            Url.direct_path(source), context.target(target))
         ).check
       }
     }
@@ -559,11 +560,13 @@
         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 options = Options.init()
         var ssh_port = 0
         var rev = ""
+        var ssh_host = ""
+        var ssh_user = ""
         var verbose = false
 
         val getopts = Getopts("""
@@ -575,30 +578,34 @@
     -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
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -p PORT      explicit SSH port
     -r REV       explicit revision (default: state of working directory)
+    -s HOST      SSH host name for remote target (default: local)
+    -u USER      explicit SSH user name
     -v           verbose
 
   Synchronize Mercurial repository with TARGET directory,
-  which can be local or remote (using notation of rsync).
+  which can be local or remote (see options -s -p -u).
 """,
           "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),
+          "o:" -> (arg => options = options + arg),
           "p:" -> (arg => ssh_port = Value.Int.parse(arg)),
           "r:" -> (arg => rev = arg),
+          "s:" -> (arg => ssh_host = arg),
+          "u:" -> (arg => ssh_user = arg),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
         val target =
           more_args match {
-            case List(target) => target
+            case List(target) => Path.explode(target)
             case _ => getopts.usage()
           }
 
@@ -608,9 +615,12 @@
             case Some(dir) => repository(dir)
             case None => the_repository(Path.current)
           }
-        val context = Rsync.Context(progress, ssh_port = ssh_port,
-          ssh_control_path = ssh_control_path, protect_args = protect_args)
-        hg.sync(context, target, thorough = thorough, dry_run = dry_run, filter = filter, rev = rev)
+
+        using(SSH.open_system(options, host = ssh_host, port = ssh_port, user = ssh_user)) { ssh =>
+          val context = Rsync.Context(progress, ssh = ssh, protect_args = protect_args)
+          hg.sync(context, target, thorough = thorough, dry_run = dry_run,
+            filter = filter, rev = rev)
+        }
       }
     )
 }
diff -r 127d077cccfe -r fb61887c069a src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Sat Apr 08 10:24:54 2023 +0200
+++ b/src/Pure/General/rsync.scala	Sat Apr 08 16:37:54 2023 +0200
@@ -9,17 +9,22 @@
 
 object Rsync {
   sealed case class Context(progress: Progress,
-    ssh_port: Int = 0,
-    ssh_control_path: String = "",
+    ssh: SSH.System = SSH.Local,
     archive: Boolean = true,
     protect_args: Boolean = true  // requires rsync 3.0.0, or later
   ) {
     def command: String = {
-      val ssh_command = SSH.client_command(port = ssh_port, control_path = ssh_control_path)
-      "rsync --rsh=" + Bash.string(ssh_command) +
+      val ssh_command = ssh.client_command
+      "rsync" +
+        if_proper(ssh_command, " --rsh=" + Bash.string(ssh_command)) +
         (if (archive) " --archive" else "") +
         (if (protect_args) " --protect-args" else "")
     }
+
+    def target(path: Path, direct: Boolean = false): String = {
+      val s = ssh.rsync_path(path)
+      if (direct) Url.direct_path(s) else s
+    }
   }
 
   def exec(
@@ -46,7 +51,7 @@
     progress.bash(script, echo = true)
   }
 
-  def init(context: Context, target: String,
+  def init(context: Context, target: Path,
     contents: List[File.Content] = Nil
   ): Unit =
     Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
@@ -56,6 +61,6 @@
         thorough = true,
         args =
           List(if (contents.nonEmpty) "--archive" else "--dirs",
-            File.bash_path(init_dir) + "/.", target)).check
+            File.bash_path(init_dir) + "/.", context.target(target))).check
     }
 }
diff -r 127d077cccfe -r fb61887c069a src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sat Apr 08 10:24:54 2023 +0200
+++ b/src/Pure/General/ssh.scala	Sat Apr 08 16:37:54 2023 +0200
@@ -113,6 +113,8 @@
     override def toString: String = user_prefix + host + port_suffix
     override def print: String = " (ssh " + toString + ")"
     override def hg_url: String = "ssh://" + toString + "/"
+    override def client_command: String =
+      SSH.client_command(port = port, control_path = control_path)
     override def rsync_prefix: String = user_prefix + host + ":"
 
 
@@ -371,6 +373,16 @@
 
   /* system operations */
 
+  def open_system(
+    options: Options,
+    host: String,
+    port: Int = 0,
+    user: String = ""
+  ): System = {
+    if (host.isEmpty) Local
+    else open_session(options, host = host, port = port, user = user)
+  }
+
   trait System extends AutoCloseable {
     def is_local: Boolean
 
@@ -379,6 +391,7 @@
     override def toString: String = "SSH.Local"
     def print: String = ""
     def hg_url: String = ""
+    def client_command: String = ""
 
     def rsync_prefix: String = ""
     def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode
diff -r 127d077cccfe -r fb61887c069a src/Pure/Tools/sync.scala
--- a/src/Pure/Tools/sync.scala	Sat Apr 08 10:24:54 2023 +0200
+++ b/src/Pure/Tools/sync.scala	Sat Apr 08 16:37:54 2023 +0200
@@ -33,7 +33,7 @@
 
   /* sync */
 
-  def sync(options: Options, context: Rsync.Context, target: String,
+  def sync(options: Options, context: Rsync.Context, target: Path,
     thorough: Boolean = false,
     purge_heaps: Boolean = false,
     session_images: List[String] = Nil,
@@ -50,7 +50,7 @@
 
     val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil
 
-    def sync(hg: Mercurial.Repository, dest: String, r: String,
+    def sync(hg: Mercurial.Repository, dest: Path, r: String,
       contents: List[File.Content] = Nil, filter: List[String] = Nil
     ): Unit = {
       hg.sync(context, dest, rev = r, thorough = thorough, dry_run = dry_run,
@@ -65,7 +65,7 @@
 
     for (hg <- afp_hg) {
       progress.echo("\n* AFP repository:", verbose = true)
-      sync(hg, Url.append_path(target, "AFP"), afp_rev)
+      sync(hg, target + Path.explode("AFP"), afp_rev)
     }
 
     val images =
@@ -73,7 +73,7 @@
         dirs = afp_root.map(_ + Path.explode("thys")).toList)
     if (images.nonEmpty) {
       progress.echo("\n* Session images:", verbose = true)
-      val heaps = Url.append_path(target, "heaps/")
+      val heaps = context.target(target + Path.explode("heaps")) + "/"
       Rsync.exec(context, thorough = thorough, dry_run = dry_run,
         args = List("--relative", "--") ::: images ::: List(heaps)).check
     }
@@ -92,7 +92,8 @@
         var dry_run = false
         var ssh_port = 0
         var rev = ""
-        var ssh_control_path = ""
+        var ssh_host = ""
+        var ssh_user = ""
         var verbose = false
 
         val getopts = Getopts("""
@@ -105,11 +106,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)
+    -s HOST      SSH host name for remote target (default: local)
+    -u USER      explicit SSH user name
     -n           no changes: dry-run
-    -p PORT      SSH port
+    -p PORT      explicit SSH port
     -r REV       explicit revision (default: state of working directory)
     -v           verbose
 
@@ -120,29 +122,31 @@
           "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),
+          "s:" -> (arg => ssh_host = arg),
+          "u:" -> (arg => ssh_user = arg),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
         val target =
           more_args match {
-            case List(target) => target
+            case List(target) => Path.explode(target)
             case _ => getopts.usage()
           }
 
         val options = Options.init()
         val progress = new Console_Progress(verbose = verbose)
-        val context =
-          Rsync.Context(progress, ssh_port = ssh_port, ssh_control_path = ssh_control_path,
-            protect_args = protect_args)
-        sync(options, context, target, 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)
+
+        using(SSH.open_system(options, host = ssh_host, port = ssh_port, user = ssh_user)) { ssh =>
+          val context = Rsync.Context(progress, ssh = ssh, protect_args = protect_args)
+          sync(options, context, target, 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)
+        }
       }
     )
 }