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