# HG changeset patch
# User wenzelm
# Date 1680970100 -7200
# Node ID c2ce9ac85859d6b7c81496499c091e0d0a7a586b
# Parent  b20ac2c26ea37d3c9c1e0f809b87242e6744e585
use remote copy of locally installed rsync component: for uniform version and options;

diff -r b20ac2c26ea3 -r c2ce9ac85859 src/Pure/Admin/component_rsync.scala
--- a/src/Pure/Admin/component_rsync.scala	Sat Apr 08 17:20:15 2023 +0200
+++ b/src/Pure/Admin/component_rsync.scala	Sat Apr 08 18:08:20 2023 +0200
@@ -10,7 +10,14 @@
 object Component_Rsync {
   /* resources */
 
-  def component_home: Path = Path.explode("$ISABELLE_RSYNC_HOME")
+  def home: Path = Path.explode("$ISABELLE_RSYNC_HOME")
+
+  def local_program: Path = Path.explode("$ISABELLE_RSYNC")
+
+  def remote_program(directory: Components.Directory): Path = {
+    val platform = "platform_" + directory.ssh.isabelle_platform.ISABELLE_PLATFORM64
+    directory.path + Path.basic(platform) + Path.basic("rsync")
+  }
 
 
   /* build rsync */
diff -r b20ac2c26ea3 -r c2ce9ac85859 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Apr 08 17:20:15 2023 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Apr 08 18:08:20 2023 +0200
@@ -53,7 +53,8 @@
           Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev())))
 
         Isabelle_System.bash(
-          """rsync -a --include="*/" --include="plain_identify*" --exclude="*" """ +
+          File.bash_path(Component_Rsync.local_program) +
+            """ -a --include="*/" --include="plain_identify*" --exclude="*" """ +
             Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check
 
         if (!Isabelle_Devel.cronjob_log.is_file)
@@ -64,7 +65,8 @@
     Logger_Task("exit",
       { logger =>
         Isabelle_System.bash(
-          "rsync -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.")
+          File.bash_path(Component_Rsync.local_program) +
+            " -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.")
             .check
       })
 
diff -r b20ac2c26ea3 -r c2ce9ac85859 src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Sat Apr 08 17:20:15 2023 +0200
+++ b/src/Pure/General/rsync.scala	Sat Apr 08 18:08:20 2023 +0200
@@ -14,22 +14,29 @@
       ssh: SSH.System = SSH.Local,
       archive: Boolean = true,
       protect_args: Boolean = true  // requires rsync 3.0.0, or later
-    ): Context = new Context(progress, ssh, archive, protect_args)
+    ): Context = {
+      val directory = Components.provide(Component_Rsync.home, ssh = ssh, progress = progress)
+      val remote_program = Component_Rsync.remote_program(directory)
+      val rsync_path = quote(File.standard_path(remote_program))
+      new Context(progress, ssh, rsync_path, archive, protect_args)
+    }
   }
 
   final class Context private(
     val progress: Progress,
     val ssh: SSH.System,
+    rsync_path: String,
     archive: Boolean,
-    protect_args: Boolean
+    protect_args: Boolean,
   ) {
-    def no_progress: Context = new Context(new Progress, ssh, archive, protect_args)
-    def no_archive: Context = new Context(progress, ssh, false, protect_args)
+    def no_progress: Context = new Context(new Progress, ssh, rsync_path, archive, protect_args)
+    def no_archive: Context = new Context(progress, ssh, rsync_path, false, protect_args)
 
     def command: String = {
       val ssh_command = ssh.client_command
-      "rsync" +
+      File.bash_path(Component_Rsync.local_program) +
         if_proper(ssh_command, " --rsh=" + Bash.string(ssh_command)) +
+        " --rsync-path=" + Bash.string(rsync_path) +
         (if (archive) " --archive" else "") +
         (if (protect_args) " --protect-args" else "")
     }