# HG changeset patch # User wenzelm # Date 1654615482 -7200 # Node ID 31abccc97adef3d7ebe572da3a4546b2684ecf22 # Parent e1b0a53328fd8ec237549c785de5bebc83c5d1fc# Parent 96fb1f9a404285b0eef0b7ceb86f7a4af68c060c merged diff -r e1b0a53328fd -r 31abccc97ade etc/build.props --- a/etc/build.props Tue Jun 07 17:20:56 2022 +0200 +++ b/etc/build.props Tue Jun 07 17:24:42 2022 +0200 @@ -83,6 +83,7 @@ src/Pure/General/pretty.scala \ src/Pure/General/properties.scala \ src/Pure/General/rdf.scala \ + src/Pure/General/rsync.scala \ src/Pure/General/scan.scala \ src/Pure/General/sha1.scala \ src/Pure/General/sql.scala \ diff -r e1b0a53328fd -r 31abccc97ade src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Tue Jun 07 17:20:56 2022 +0200 +++ b/src/Pure/Admin/build_history.scala Tue Jun 07 17:24:42 2022 +0200 @@ -522,6 +522,7 @@ isabelle_other: Path, isabelle_identifier: String = "remote_build_history", progress: Progress = new Progress, + protect_args: Boolean = false, rev: String = "", afp_repos: Option[Path] = None, afp_rev: String = "", @@ -534,7 +535,8 @@ def sync_repos(target: Path, accurate: Boolean = false, rev: String = "", afp_rev: String = "", afp: Boolean = false ): Unit = { - Sync_Repos.sync_repos(ssh.rsync_path(target), port = ssh.port, progress = progress, + val context = Rsync.Context(progress, port = ssh.port, protect_args = protect_args) + Sync_Repos.sync_repos(context, ssh.rsync_path(target), thorough = accurate, preserve_jars = !accurate, rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None) } diff -r e1b0a53328fd -r 31abccc97ade src/Pure/Admin/sync_repos.scala --- a/src/Pure/Admin/sync_repos.scala Tue Jun 07 17:20:56 2022 +0200 +++ b/src/Pure/Admin/sync_repos.scala Tue Jun 07 17:24:42 2022 +0200 @@ -8,9 +8,7 @@ object Sync_Repos { - def sync_repos(target: String, - progress: Progress = new Progress, - port: Int = SSH.default_port, + def sync_repos(context: Rsync.Context, target: String, verbose: Boolean = false, thorough: Boolean = false, preserve_jars: Boolean = false, @@ -27,18 +25,18 @@ def sync(hg: Mercurial.Repository, dest: String, r: String, contents: List[File.Content] = Nil, filter: List[String] = Nil ): Unit = { - hg.sync(dest, rev = r, progress = progress, port = port, verbose = verbose, - thorough = thorough, dry_run = dry_run, contents = contents, filter = filter ::: more_filter) + hg.sync(context, dest, rev = r, verbose = verbose, thorough = thorough, dry_run = dry_run, + contents = contents, filter = filter ::: more_filter) } - progress.echo_if(verbose, "\n* Isabelle repository:") + context.progress.echo_if(verbose, "\n* Isabelle repository:") sync(hg, target, rev, contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))), filter = List("protect /AFP")) for (hg <- afp_hg) { - progress.echo_if(verbose, "\n* AFP repository:") - sync(hg, Isabelle_System.rsync_dir(target) + "/AFP", afp_rev) + context.progress.echo_if(verbose, "\n* AFP repository:") + sync(hg, Rsync.append(target, "AFP"), afp_rev) } } @@ -94,7 +92,8 @@ } val progress = new Console_Progress - sync_repos(target, progress = progress, port = port, verbose = verbose, thorough = thorough, + val context = Rsync.Context(progress, port = port) + sync_repos(context, target, verbose = verbose, thorough = thorough, preserve_jars = preserve_jars, dry_run = dry_run, rev = rev, afp_root = afp_root, afp_rev = afp_rev) } diff -r e1b0a53328fd -r 31abccc97ade src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Tue Jun 07 17:20:56 2022 +0200 +++ b/src/Pure/General/mercurial.scala Tue Jun 07 17:24:42 2022 +0200 @@ -293,9 +293,7 @@ def known_files(): List[String] = status(options = "--modified --added --clean --no-status") - def sync(target: String, - progress: Progress = new Progress, - port: Int = SSH.default_port, + def sync(context: Rsync.Context, target: String, verbose: Boolean = false, thorough: Boolean = false, dry_run: Boolean = false, @@ -306,11 +304,11 @@ require(ssh == SSH.Local, "local repository required") Isabelle_System.with_tmp_dir("sync") { tmp_dir => - Isabelle_System.rsync_init(target, port = port) + Rsync.init(context, target) val list = - Isabelle_System.rsync(port = port, list = true, - args = List("--", Isabelle_System.rsync_dir(target)) + Rsync.exec(context, list = true, + args = List("--", Rsync.terminate(target)) ).check.out_lines.filterNot(_.endsWith(" .")) if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) { error("No .hg_sync meta data in " + quote(target)) @@ -322,7 +320,7 @@ val diff_content = if (is_changed) diff(rev = rev, options = "--git") else "" val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else "" - Isabelle_System.rsync_init(target, port = port, + Rsync.init(context, target, contents = File.Content(Hg_Sync.PATH_ID, id_content) :: File.Content(Hg_Sync.PATH_LOG, log_content) :: @@ -348,14 +346,15 @@ val protect = (Hg_Sync.PATH :: contents.map(_.path)) .map(path => "protect /" + File.standard_path(path)) - Isabelle_System.rsync( - progress = progress, port = port, verbose = verbose, thorough = thorough, + Rsync.exec(context, + verbose = verbose, + thorough = thorough, dry_run = dry_run, clean = true, prune_empty_dirs = true, filter = protect ::: filter, args = List("--exclude-from=" + exclude_path.implode, "--", - Isabelle_System.rsync_dir(source), target) + Rsync.terminate(source), target) ).check } } @@ -606,7 +605,8 @@ case Some(dir) => repository(dir) case None => the_repository(Path.current) } - hg.sync(target, progress = progress, port = port, verbose = verbose, thorough = thorough, + val context = Rsync.Context(progress, port = port) + hg.sync(context, target, verbose = verbose, thorough = thorough, dry_run = dry_run, filter = filter, rev = rev) } ) diff -r e1b0a53328fd -r 31abccc97ade src/Pure/General/rsync.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/rsync.scala Tue Jun 07 17:24:42 2022 +0200 @@ -0,0 +1,64 @@ +/* Title: Pure/General/rsync.scala + Author: Makarius + +Support for rsync: see also https://rsync.samba.org +*/ + +package isabelle + + +object Rsync { + sealed case class Context(progress: Progress, + port: Int = SSH.default_port, + archive: Boolean = true, + protect_args: Boolean = true + ) { + def command: String = + "rsync --rsh=" + Bash.string("ssh -p " + port) + + (if (archive) " --archive" else "") + + (if (protect_args) " --protect-args" else "") + } + + def exec( + context: Context, + verbose: Boolean = false, + thorough: Boolean = false, + prune_empty_dirs: Boolean = false, + dry_run: Boolean = false, + clean: Boolean = false, + list: Boolean = false, + filter: List[String] = Nil, + args: List[String] = Nil + ): Process_Result = { + val script = + context.command + + (if (verbose) " --verbose" else "") + + (if (thorough) " --ignore-times" else " --omit-dir-times") + + (if (prune_empty_dirs) " --prune-empty-dirs" else "") + + (if (dry_run) " --dry-run" else "") + + (if (clean) " --delete-excluded" else "") + + (if (list) " --list-only --no-human-readable" else "") + + filter.map(s => " --filter=" + Bash.string(s)).mkString + + (if (args.nonEmpty) " " + Bash.strings(args) else "") + context.progress.bash(script, echo = true) + } + + def init(context: Context, target: String, + contents: List[File.Content] = Nil + ): Unit = + Isabelle_System.with_tmp_dir("sync") { tmp_dir => + val init_dir = Isabelle_System.make_directory(tmp_dir + Path.explode("init")) + contents.foreach(_.write(init_dir)) + exec(context, thorough = true, + args = List(File.bash_path(init_dir) + "/.", target)).check + } + + def terminate(target: String): String = + if (target.endsWith(":") || target.endsWith("/")) target + "." + else if (target.endsWith(":.") || target.endsWith("/.")) target + else target + "/." + + def append(target: String, rest: String): String = + if (target.endsWith(":") || target.endsWith("/")) target + rest + else target + "/" + rest +} diff -r e1b0a53328fd -r 31abccc97ade src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Tue Jun 07 17:20:56 2022 +0200 +++ b/src/Pure/System/isabelle_system.scala Tue Jun 07 17:24:42 2022 +0200 @@ -420,48 +420,6 @@ else error("Expected to find GNU tar executable") } - def rsync( - progress: Progress = new Progress, - port: Int = SSH.default_port, - verbose: Boolean = false, - thorough: Boolean = false, - prune_empty_dirs: Boolean = false, - dry_run: Boolean = false, - clean: Boolean = false, - list: Boolean = false, - filter: List[String] = Nil, - args: List[String] = Nil - ): Process_Result = { - val script = - "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) + - (if (verbose) " --verbose" else "") + - (if (thorough) " --ignore-times" else " --omit-dir-times") + - (if (prune_empty_dirs) " --prune-empty-dirs" else "") + - (if (dry_run) " --dry-run" else "") + - (if (clean) " --delete-excluded" else "") + - (if (list) " --list-only --no-human-readable" else "") + - filter.map(s => " --filter=" + Bash.string(s)).mkString + - (if (args.nonEmpty) " " + Bash.strings(args) else "") - progress.bash(script, echo = true) - } - - def rsync_dir(target: String): String = { - if (target.endsWith(":.") || target.endsWith("/.")) target - else if (target.endsWith(":") || target.endsWith("/")) target + "." - else target + "/." - } - - def rsync_init(target: String, - port: Int = SSH.default_port, - contents: List[File.Content] = Nil - ): Unit = - with_tmp_dir("sync") { tmp_dir => - val init_dir = make_directory(tmp_dir + Path.explode("init")) - contents.foreach(_.write(init_dir)) - rsync(port = port, thorough = true, - args = List(File.bash_path(init_dir) + "/.", target)).check - } - def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = { with_tmp_file("patch") { patch => Isabelle_System.bash(