# HG changeset patch # User wenzelm # Date 1680975129 -7200 # Node ID b81b2c50fc7c778ad7e695c63249500e4782865e # Parent 3e72fab0e699dce3dd52c1aaffc86b75c885725e use "rsync --secluded-args" by default, discontinue obsolete option -P of sync tools; diff -r 3e72fab0e699 -r b81b2c50fc7c NEWS --- 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 diff -r 3e72fab0e699 -r b81b2c50fc7c src/Doc/System/Misc.thy --- 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>\-p\ specifies an explicit port for the SSH connection underlying \<^verbatim>\rsync\; the default is taken from the user's \<^path>\ssh_config\ file. - - \<^medskip> Option \<^verbatim>\-P\ uses \<^verbatim>\rsync --protect-args\ to work robustly with spaces or - special characters of the shell. This requires at least \<^verbatim>\rsync 3.0.0\, - 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. \ subsubsection \Examples\ diff -r 3e72fab0e699 -r b81b2c50fc7c src/Doc/System/Sessions.thy --- 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>\AFP\; thus it can be easily included elsewhere, e.g. @{tool build}~\<^verbatim>\-d\~\<^verbatim>\'~~/AFP'\ on the remote side. - \<^medskip> Options \<^verbatim>\-P\, \<^verbatim>\-T\, \<^verbatim>\-n\, \<^verbatim>\-p\, \<^verbatim>\-s\, \<^verbatim>\-u\, \<^verbatim>\-v\ are the same as + \<^medskip> Options \<^verbatim>\-T\, \<^verbatim>\-n\, \<^verbatim>\-p\, \<^verbatim>\-s\, \<^verbatim>\-u\, \<^verbatim>\-v\ are the same as the underlying @{tool hg_sync}. \<^medskip> Options \<^verbatim>\-r\ and \<^verbatim>\-a\ are the same as option \<^verbatim>\-r\ for @{tool hg_sync}, diff -r 3e72fab0e699 -r b81b2c50fc7c src/Pure/Admin/build_history.scala --- 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) diff -r 3e72fab0e699 -r b81b2c50fc7c src/Pure/General/mercurial.scala --- 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) } diff -r 3e72fab0e699 -r b81b2c50fc7c src/Pure/General/rsync.scala --- 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 = { diff -r 3e72fab0e699 -r b81b2c50fc7c src/Pure/Tools/sync.scala --- 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)