--- 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 \
--- 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)
}
--- 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)
}
--- 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)
}
)
--- /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
+}
--- 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(