--- a/src/Doc/System/Misc.thy Mon May 30 12:46:11 2022 +0100
+++ b/src/Doc/System/Misc.thy Mon May 30 12:46:22 2022 +0100
@@ -313,9 +313,10 @@
Options are:
-C clean all unknown/ignored files on target
(implies -n for testing; use option -f to confirm)
- -P NAME protect NAME within TARGET from deletion
+ -F RULE add rsync filter RULE (e.g. "protect /foo" to avoid deletion)
-R ROOT explicit repository root directory
(default: implicit from current directory)
+ -T thorough treatment of file content and directory times
-f force changes: no dry-run
-n no changes: dry-run
-r REV explicit revision (default: state of working directory)
@@ -341,20 +342,24 @@
for ``dry-run'' with verbose output. A subsequent option \<^verbatim>\<open>-f\<close> is required
to force actual deletions on the target.
- \<^medskip> Option \<^verbatim>\<open>-P\<close> protects a given file or directory from deletion; multiple
- \<^verbatim>\<open>-P\<close> options may be given to accumulate protected entries.
+ \<^medskip> Option \<^verbatim>\<open>-F\<close> adds a filter rule to the underlying \<^verbatim>\<open>rsync\<close> command;
+ multiple \<^verbatim>\<open>-F\<close> options may be given to accumulate a list of rules.
\<^medskip> Option \<^verbatim>\<open>-R\<close> specifies an explicit repository root directory. The default
is to derive it from the current directory, searching upwards until a
suitable \<^verbatim>\<open>.hg\<close> directory is found.
+
+ \<^medskip> Option \<^verbatim>\<open>-T\<close> indicates thorough treatment of file content and directory
+ times. The default is to consider files with equal time and size already as
+ equal, and to ignore time stamps on directories.
\<close>
subsubsection \<open>Examples\<close>
text \<open>
- Synchronize the Isabelle repository onto a remote host, while
- protecting a copy of AFP inside of it (without changing that):
- @{verbatim [display] \<open> isabelle hg_sync -R '$ISABELLE_HOME' -P AFP -C testmachine:test/isabelle\<close>}
+ Synchronize the current repository onto a remote host, with accurate
+ treatment of all content:
+ @{verbatim [display] \<open> isabelle hg_sync -T -C remotename:test/repos\<close>}
So far, this is only a dry run. In a realistic situation, it requires
consecutive options \<^verbatim>\<open>-C -f\<close> as confirmation.
--- a/src/Pure/Admin/build_jedit.scala Mon May 30 12:46:11 2022 +0100
+++ b/src/Pure/Admin/build_jedit.scala Mon May 30 12:46:22 2022 +0100
@@ -136,7 +136,7 @@
path
}
- Isabelle_System.with_tmp_dir("tmp") { tmp_dir =>
+ Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* original version */
val install_path = download_jedit(tmp_dir, "install.jar")
--- a/src/Pure/Admin/build_release.scala Mon May 30 12:46:11 2022 +0100
+++ b/src/Pure/Admin/build_release.scala Mon May 30 12:46:22 2022 +0100
@@ -102,7 +102,7 @@
object Release_Archive {
def make(bytes: Bytes, rename: String = ""): Release_Archive = {
- Isabelle_System.with_tmp_dir("tmp")(dir =>
+ Isabelle_System.with_tmp_dir("build_release")(dir =>
Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path =>
val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
--- a/src/Pure/Admin/build_sqlite.scala Mon May 30 12:46:11 2022 +0100
+++ b/src/Pure/Admin/build_sqlite.scala Mon May 30 12:46:22 2022 +0100
@@ -54,7 +54,7 @@
val jar = component_dir + Path.basic(download_name).ext("jar")
Isabelle_System.download_file(download_url, jar, progress = progress)
- Isabelle_System.with_tmp_dir("sqlite") { jar_dir =>
+ Isabelle_System.with_tmp_dir("build") { jar_dir =>
progress.echo("Unpacking " + jar)
Isabelle_System.bash("isabelle_jdk jar xf " + File.bash_path(jar.absolute),
cwd = jar_dir.file).check
--- a/src/Pure/Admin/sync_repos.scala Mon May 30 12:46:11 2022 +0100
+++ b/src/Pure/Admin/sync_repos.scala Mon May 30 12:46:22 2022 +0100
@@ -11,6 +11,8 @@
def sync_repos(target: String,
progress: Progress = new Progress,
verbose: Boolean = false,
+ thorough: Boolean = false,
+ preserve_jars: Boolean = false,
dry_run: Boolean = false,
clean: Boolean = false,
rev: String = "",
@@ -22,18 +24,21 @@
val isabelle_hg = Mercurial.repository(Path.ISABELLE_HOME)
val afp_hg = afp_root.map(Mercurial.repository(_))
+ val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil
+
def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit =
- hg.sync(dest, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
- rev = r, filter = filter)
+ hg.sync(dest, rev = r, progress = progress, verbose = verbose, thorough = thorough,
+ dry_run = dry_run, clean = clean, filter = filter ::: more_filter)
progress.echo("\n* Isabelle repository:")
- sync(isabelle_hg, target, rev, filter = List("protect /AFP", "protect etc/ISABELLE_ID"))
+ sync(isabelle_hg, target, rev, filter = List("protect /AFP", "protect /etc/ISABELLE_ID"))
if (!dry_run) {
- Isabelle_System.with_tmp_dir("sync_repos") { tmp_dir =>
+ Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
val id_path = tmp_dir + Path.explode("ISABELLE_ID")
File.write(id_path, isabelle_hg.id(rev = rev))
- Isabelle_System.rsync(args = List(File.standard_path(id_path), target_dir + "etc/"))
+ Isabelle_System.rsync(thorough = thorough,
+ args = List(File.standard_path(id_path), target_dir + "etc/"))
}
}
@@ -48,6 +53,8 @@
Scala_Project.here, { args =>
var afp_root: Option[Path] = None
var clean = false
+ var preserve_jars = false
+ var thorough = false
var afp_rev = ""
var dry_run = false
var rev = ""
@@ -58,8 +65,10 @@
Options are:
-A ROOT include AFP with given root directory
+ -J preserve *.jar files
-C clean all unknown/ignored files on target
(implies -n for testing; use option -f to confirm)
+ -T thorough treatment of file content and directory times
-a REV explicit AFP revision (default: state of working directory)
-f force changes: no dry-run
-n no changes: dry-run
@@ -67,9 +76,21 @@
-v verbose
Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync".
+
+ Examples (without -f as "dry-run"):
+
+ * quick testing
+
+ isabelle sync_repos -A '$AFP_BASE' -J -C testmachine:test/isabelle_afp
+
+ * accurate testing
+
+ isabelle sync_repos -A '$AFP_BASE' -T -C testmachine:test/isabelle_afp
""",
"A:" -> (arg => afp_root = Some(Path.explode(arg))),
+ "J" -> (_ => preserve_jars = true),
"C" -> { _ => clean = true; dry_run = true },
+ "T" -> (_ => thorough = true),
"a:" -> (arg => afp_rev = arg),
"f" -> (_ => dry_run = false),
"n" -> (_ => dry_run = true),
@@ -84,8 +105,9 @@
}
val progress = new Console_Progress
- sync_repos(target, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
- rev = rev, afp_root = afp_root, afp_rev = afp_rev)
+ sync_repos(target, progress = progress, verbose = verbose, thorough = thorough,
+ preserve_jars = preserve_jars, dry_run = dry_run, clean = clean, rev = rev,
+ afp_root = afp_root, afp_rev = afp_rev)
}
)
}
--- a/src/Pure/General/mercurial.scala Mon May 30 12:46:11 2022 +0100
+++ b/src/Pure/General/mercurial.scala Mon May 30 12:46:22 2022 +0100
@@ -254,6 +254,7 @@
def sync(target: String,
progress: Progress = new Progress,
verbose: Boolean = false,
+ thorough: Boolean = false,
dry_run: Boolean = false,
clean: Boolean = false,
filter: List[String] = Nil,
@@ -261,7 +262,7 @@
): Unit = {
require(ssh == SSH.Local, "local repository required")
- Isabelle_System.with_tmp_dir("rsync") { tmp_dir =>
+ Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
val (options, source) =
if (rev.isEmpty) {
val exclude_path = tmp_dir + Path.explode("exclude")
@@ -278,7 +279,8 @@
(Nil, source)
}
Isabelle_System.rsync(
- progress = progress, verbose = verbose, dry_run = dry_run, clean = clean, filter = filter,
+ progress = progress, verbose = verbose, thorough = thorough,
+ dry_run = dry_run, clean = clean, filter = filter,
args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target))
}
}
@@ -484,8 +486,9 @@
Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory",
Scala_Project.here, { args =>
var clean = false
- var protect: List[String] = Nil
+ var filter: List[String] = Nil
var root: Option[Path] = None
+ var thorough = false
var dry_run = false
var rev = ""
var verbose = false
@@ -496,9 +499,10 @@
Options are:
-C clean all unknown/ignored files on target
(implies -n for testing; use option -f to confirm)
- -P NAME protect NAME within TARGET from deletion
+ -F RULE add rsync filter RULE (e.g. "protect /foo" to avoid deletion)
-R ROOT explicit repository root directory
(default: implicit from current directory)
+ -T thorough treatment of file content and directory times
-f force changes: no dry-run
-n no changes: dry-run
-r REV explicit revision (default: state of working directory)
@@ -508,8 +512,9 @@
which can be local or remote (using notation of rsync).
""",
"C" -> { _ => clean = true; dry_run = true },
- "P:" -> (arg => protect = protect ::: List(arg)),
+ "F:" -> (arg => filter = filter ::: List(arg)),
"R:" -> (arg => root = Some(Path.explode(arg))),
+ "T" -> (_ => thorough = true),
"f" -> (_ => dry_run = false),
"n" -> (_ => dry_run = true),
"r:" -> (arg => rev = arg),
@@ -528,8 +533,8 @@
case Some(dir) => repository(dir)
case None => the_repository(Path.current)
}
- hg.sync(target, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
- filter = protect.map("protect /" + _), rev = rev)
+ hg.sync(target, progress = progress, verbose = verbose, thorough = thorough,
+ dry_run = dry_run, clean = clean, filter = filter, rev = rev)
}
)
}
--- a/src/Pure/System/isabelle_system.scala Mon May 30 12:46:11 2022 +0100
+++ b/src/Pure/System/isabelle_system.scala Mon May 30 12:46:22 2022 +0100
@@ -424,6 +424,7 @@
cwd: JFile = null,
progress: Progress = new Progress,
verbose: Boolean = false,
+ thorough: Boolean = false,
dry_run: Boolean = false,
clean: Boolean = false,
filter: List[String] = Nil,
@@ -432,6 +433,7 @@
val script =
"rsync --protect-args --archive" +
(if (verbose || dry_run) " --verbose" else "") +
+ (if (thorough) " --ignore-times" else " --omit-dir-times") +
(if (dry_run) " --dry-run" else "") +
(if (clean) " --delete-excluded" else "") +
filter.map(s => " --filter=" + Bash.string(s)).mkString +