# HG changeset patch
# User paulson
# Date 1653911182 -3600
# Node ID 4f9809edf95ad18fd15499ecff7e4937039c01c1
# Parent  f775dfb556552be002c3e5e9b15f7fe4c91199e1# Parent  eded3fe9e600f04a4d9d8930908b6cf45d4ea3e6
merged

diff -r eded3fe9e600 -r 4f9809edf95a src/Doc/System/Misc.thy
--- 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.
diff -r eded3fe9e600 -r 4f9809edf95a src/Pure/Admin/build_jedit.scala
--- 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")
diff -r eded3fe9e600 -r 4f9809edf95a src/Pure/Admin/build_release.scala
--- 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)
 
diff -r eded3fe9e600 -r 4f9809edf95a src/Pure/Admin/build_sqlite.scala
--- 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
diff -r eded3fe9e600 -r 4f9809edf95a src/Pure/Admin/sync_repos.scala
--- 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)
       }
     )
 }
diff -r eded3fe9e600 -r 4f9809edf95a src/Pure/General/mercurial.scala
--- 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)
       }
     )
 }
diff -r eded3fe9e600 -r 4f9809edf95a src/Pure/System/isabelle_system.scala
--- 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 +