use "rsync --secluded-args" by default, discontinue obsolete option -P of sync tools;
--- a/NEWS Sat Apr 08 19:02:51 2023 +0200
+++ b/NEWS Sat Apr 08 19:32:09 2023 +0200
@@ -305,6 +305,12 @@
*** System ***
+* The "rsync" tool has been bundled as Isabelle component, with uniform
+version and compilation options on all platforms. This allows to use
+more recent options for extra robustness, notably "--secluded-args"
+(formerly "--protected-args"). Option -P of "isabelle hg_sync" and
+"isabelle sync" has been eliminated accordingly.
+
* 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
--- a/src/Doc/System/Misc.thy Sat Apr 08 19:02:51 2023 +0200
+++ b/src/Doc/System/Misc.thy Sat Apr 08 19:32:09 2023 +0200
@@ -320,7 +320,6 @@
Options are:
-F RULE add rsync filter RULE
(e.g. "protect /foo" to avoid deletion)
- -P protect spaces in target file names: more robust, less portable
-R ROOT explicit repository root directory
(default: implicit from current directory)
-T thorough treatment of file content and directory times
@@ -368,12 +367,6 @@
\<^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>-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
- Unix-style naming of files and directories, it is safe to omit this option
- for the sake of portability.
\<close>
subsubsection \<open>Examples\<close>
--- a/src/Doc/System/Sessions.thy Sat Apr 08 19:02:51 2023 +0200
+++ b/src/Doc/System/Sessions.thy Sat Apr 08 19:32:09 2023 +0200
@@ -936,7 +936,6 @@
-I NAME include session heap image and build database
(based on accidental local state)
-J preserve *.jar files
- -P protect spaces in target file names: more robust, less portable
-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)
@@ -957,7 +956,7 @@
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>-s\<close>, \<^verbatim>\<open>-u\<close>, \<^verbatim>\<open>-v\<close> are the same as
+ \<^medskip> Options \<^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},
--- a/src/Pure/Admin/build_history.scala Sat Apr 08 19:02:51 2023 +0200
+++ b/src/Pure/Admin/build_history.scala Sat Apr 08 19:32:09 2023 +0200
@@ -535,7 +535,6 @@
clean_platform: Boolean = false,
clean_archives: Boolean = false,
progress: Progress = new Progress,
- protect_args: Boolean = false,
rev: String = "",
afp_repos: Option[Path] = None,
afp_rev: String = "",
@@ -548,7 +547,7 @@
def sync(target: Path, accurate: Boolean = false,
rev: String = "", afp_rev: String = "", afp: Boolean = false
): Unit = {
- val context = Rsync.Context(progress = progress, ssh = ssh, protect_args = protect_args)
+ val context = Rsync.Context(progress = progress, ssh = ssh)
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 19:02:51 2023 +0200
+++ b/src/Pure/General/mercurial.scala Sat Apr 08 19:32:09 2023 +0200
@@ -552,7 +552,6 @@
Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory",
Scala_Project.here, { args =>
var filter: List[String] = Nil
- var protect_args = false
var root: Option[Path] = None
var thorough = false
var dry_run = false
@@ -569,7 +568,6 @@
Options are:
-F RULE add rsync filter RULE
(e.g. "protect /foo" to avoid deletion)
- -P protect spaces in target file names: more robust, less portable
-R ROOT explicit repository root directory
(default: implicit from current directory)
-T thorough treatment of file content and directory times
@@ -585,7 +583,6 @@
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))),
"T" -> (_ => thorough = true),
"n" -> (_ => dry_run = true),
@@ -611,7 +608,7 @@
}
using(SSH.open_system(options, host = ssh_host, port = ssh_port, user = ssh_user)) { ssh =>
- val context = Rsync.Context(progress = progress, ssh = ssh, protect_args = protect_args)
+ val context = Rsync.Context(progress = progress, ssh = ssh)
hg.sync(context, target, thorough = thorough, dry_run = dry_run,
filter = filter, rev = rev)
}
--- a/src/Pure/General/rsync.scala Sat Apr 08 19:02:51 2023 +0200
+++ b/src/Pure/General/rsync.scala Sat Apr 08 19:32:09 2023 +0200
@@ -12,11 +12,10 @@
def apply(
progress: Progress = new Progress,
ssh: SSH.System = SSH.Local,
- archive: Boolean = true,
- protect_args: Boolean = true // requires rsync 3.0.0, or later
+ archive: Boolean = true
): Context = {
val directory = Components.provide(Component_Rsync.home, ssh = ssh, progress = progress)
- new Context(directory, progress, archive, protect_args)
+ new Context(directory, progress, archive)
}
}
@@ -24,23 +23,21 @@
directory: Components.Directory,
val progress: Progress,
archive: Boolean,
- protect_args: Boolean,
) {
override def toString: String = directory.toString
- def no_progress: Context = new Context(directory, new Progress, archive, protect_args)
- def no_archive: Context = new Context(directory, progress, false, protect_args)
+ def no_progress: Context = new Context(directory, new Progress, archive)
+ def no_archive: Context = new Context(directory, progress, false)
def ssh: SSH.System = directory.ssh
def command: String = {
val program = Component_Rsync.remote_program(directory)
val ssh_command = ssh.client_command
- File.bash_path(Component_Rsync.local_program) +
+ File.bash_path(Component_Rsync.local_program) + " --secluded-args" +
if_proper(ssh_command, " --rsh=" + Bash.string(ssh_command)) +
" --rsync-path=" + Bash.string(quote(File.standard_path(program))) +
- (if (archive) " --archive" else "") +
- (if (protect_args) " --protect-args" else "")
+ (if (archive) " --archive" else "")
}
def target(path: Path, direct: Boolean = false): String = {
--- a/src/Pure/Tools/sync.scala Sat Apr 08 19:02:51 2023 +0200
+++ b/src/Pure/Tools/sync.scala Sat Apr 08 19:32:09 2023 +0200
@@ -86,7 +86,6 @@
var purge_heaps = false
var session_images = List.empty[String]
var preserve_jars = false
- var protect_args = false
var thorough = false
var afp_rev = ""
var dry_run = false
@@ -105,7 +104,6 @@
-I NAME include session heap image and build database
(based on accidental local state)
-J preserve *.jar files
- -P protect spaces in target file names: more robust, less portable
-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)
@@ -121,7 +119,6 @@
"H" -> (_ => purge_heaps = true),
"I:" -> (arg => session_images = session_images ::: List(arg)),
"J" -> (_ => preserve_jars = true),
- "P" -> (_ => protect_args = true),
"T" -> (_ => thorough = true),
"a:" -> (arg => afp_rev = arg),
"n" -> (_ => dry_run = true),
@@ -142,7 +139,7 @@
val progress = new Console_Progress(verbose = verbose)
using(SSH.open_system(options, host = ssh_host, port = ssh_port, user = ssh_user)) { ssh =>
- val context = Rsync.Context(progress = progress, ssh = ssh, protect_args = protect_args)
+ val context = Rsync.Context(progress = progress, ssh = ssh)
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)