# HG changeset patch
# User wenzelm
# Date 1653857254 -7200
# Node ID b1748f6ca6c867cb9a91d9694b82ec6a2d5e0058
# Parent  9e34819a7ca18e637025e2bb87ed5d3d90058ef8# Parent  029cd4e1a2c741de1c173be98206eb0400f9dfd2
merged

diff -r 9e34819a7ca1 -r b1748f6ca6c8 NEWS
--- a/NEWS	Sat May 28 10:45:45 2022 +0200
+++ b/NEWS	Sun May 29 22:47:34 2022 +0200
@@ -1,3 +1,4 @@
+
 Isabelle NEWS -- history of user-relevant changes
 =================================================
 
@@ -119,6 +120,10 @@
 explicitly. This increases the chances that the Java/Scala IDE project
 works properly.
 
+* Command-line tool "isabelle hg_sync" synchronizes the working
+directory of a local Mercurial repository with a target directory, using
+rsync notation for destinations.
+
 
 
 New in Isabelle2021-1 (December 2021)
diff -r 9e34819a7ca1 -r b1748f6ca6c8 etc/build.props
--- a/etc/build.props	Sat May 28 10:45:45 2022 +0200
+++ b/etc/build.props	Sun May 29 22:47:34 2022 +0200
@@ -38,6 +38,7 @@
   src/Pure/Admin/isabelle_devel.scala \
   src/Pure/Admin/jenkins.scala \
   src/Pure/Admin/other_isabelle.scala \
+  src/Pure/Admin/sync_repos.scala \
   src/Pure/Concurrent/consumer_thread.scala \
   src/Pure/Concurrent/counter.scala \
   src/Pure/Concurrent/delay.scala \
diff -r 9e34819a7ca1 -r b1748f6ca6c8 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Sat May 28 10:45:45 2022 +0200
+++ b/src/Doc/System/Misc.thy	Sun May 29 22:47:34 2022 +0200
@@ -300,6 +300,67 @@
 \<close>
 
 
+section \<open>Mercurial repository synchronization\<close>
+
+text \<open>
+  The @{tool_def hg_sync} tool synchronizes a local Mercurial repository with
+  a target directory, using \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close>
+  notation for destinations.
+
+  @{verbatim [display]
+\<open>Usage: isabelle hg_sync [OPTIONS] TARGET
+
+  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
+    -R ROOT      explicit repository root directory
+                 (default: implicit from current directory)
+    -f           force changes: no dry-run
+    -n           no changes: dry-run
+    -r REV       explicit revision (default: state of working directory)
+    -v           verbose
+
+  Synchronize Mercurial repository with TARGET directory,
+  which can be local or remote (using notation of rsync).\<close>}
+
+  The \<^verbatim>\<open>TARGET\<close> specification can be a local or remote directory (via ssh),
+  using \<^verbatim>\<open>rsync\<close> notation (see examples below). The content is written
+  directly into the target, \<^emph>\<open>without\<close> creating a separate sub-directory.
+
+  \<^medskip> Option \<^verbatim>\<open>-r\<close> specifies an explicit revision of the repository; the default
+  is the current state of the working directory (which might be uncommitted).
+
+  \<^medskip> Option \<^verbatim>\<open>-v\<close> enables verbose mode. Option \<^verbatim>\<open>-n\<close> enables ``dry-run'' mode:
+  operations are only simulated and printed as in verbose mode. Option \<^verbatim>\<open>-f\<close>
+  disables ``dry-run'' mode and thus forces changes to be applied.
+
+  \<^medskip> Option \<^verbatim>\<open>-C\<close> causes deletion of all unknown/ignored files on the target.
+  This is potentially dangerous: giving a wrong target directory will cause
+  its total destruction! For robustness, option \<^verbatim>\<open>-C\<close> implies option \<^verbatim>\<open>-n\<close>,
+  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>-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.
+\<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>}
+
+  So far, this is only a dry run. In a realistic situation, it requires
+  consecutive options \<^verbatim>\<open>-C -f\<close> as confirmation.
+\<close>
+
+
 section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close>
 
 text \<open>
diff -r 9e34819a7ca1 -r b1748f6ca6c8 src/Pure/Admin/build_cygwin.scala
--- a/src/Pure/Admin/build_cygwin.scala	Sat May 28 10:45:45 2022 +0200
+++ b/src/Pure/Admin/build_cygwin.scala	Sun May 29 22:47:34 2022 +0200
@@ -11,7 +11,7 @@
   val default_mirror: String = "https://isabelle.sketis.net/cygwin_2021-1"
 
   val packages: List[String] =
-    List("curl", "libgmp-devel", "nano", "unzip")
+    List("curl", "libgmp-devel", "nano", "rsync", "unzip")
 
   def build_cygwin(progress: Progress,
     mirror: String = default_mirror,
diff -r 9e34819a7ca1 -r b1748f6ca6c8 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Sat May 28 10:45:45 2022 +0200
+++ b/src/Pure/Admin/build_release.scala	Sun May 29 22:47:34 2022 +0200
@@ -412,7 +412,7 @@
 
       Isabelle_System.new_directory(context.dist_dir)
 
-      hg.archive(context.isabelle_dir.expand.implode, rev = id, options = "--type files")
+      hg.archive(context.isabelle_dir.expand.implode, rev = id)
 
       for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
         (context.isabelle_dir + Path.explode(name)).file.delete
diff -r 9e34819a7ca1 -r b1748f6ca6c8 src/Pure/Admin/sync_repos.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/sync_repos.scala	Sun May 29 22:47:34 2022 +0200
@@ -0,0 +1,92 @@
+/*  Title:      Pure/Admin/sync_repos.scala
+    Author:     Makarius
+
+Synchronize Isabelle + AFP repositories.
+*/
+
+package isabelle
+
+
+object Sync_Repos {
+  def sync_repos(target: String,
+    progress: Progress = new Progress,
+    verbose: Boolean = false,
+    dry_run: Boolean = false,
+    clean: Boolean = false,
+    rev: String = "",
+    afp_root: Option[Path] = None,
+    afp_rev: String = ""
+  ): Unit = {
+    val target_dir = if (target.endsWith(":") || target.endsWith("/")) target else target + "/"
+
+    val isabelle_hg = Mercurial.repository(Path.ISABELLE_HOME)
+    val afp_hg = afp_root.map(Mercurial.repository(_))
+
+    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)
+
+    progress.echo("\n* Isabelle repository:")
+    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 =>
+        val id_path = tmp_dir + Path.explode("ISABELLE_ID")
+        File.write(id_path, isabelle_hg.id(rev = rev))
+        Isabelle_System.rsync(progress = progress, verbose = verbose,
+          args = List(File.standard_path(id_path), target_dir + "etc/")).check
+      }
+    }
+
+    for (hg <- afp_hg) {
+      progress.echo("\n* AFP repository:")
+      sync(hg, target_dir + "AFP", afp_rev)
+    }
+  }
+
+  val isabelle_tool =
+    Isabelle_Tool("sync_repos", "synchronize Isabelle + AFP repositories",
+      Scala_Project.here, { args =>
+        var afp_root: Option[Path] = None
+        var clean = false
+        var afp_rev = ""
+        var dry_run = false
+        var rev = ""
+        var verbose = false
+
+        val getopts = Getopts("""
+Usage: isabelle sync_repos [OPTIONS] TARGET
+
+  Options are:
+    -A ROOT      include AFP with given root directory
+    -C           clean all unknown/ignored files on target
+                 (implies -n for testing; use option -f to confirm)
+    -a REV       explicit AFP revision (default: state of working directory)
+    -f           force changes: no dry-run
+    -n           no changes: dry-run
+    -r REV       explicit revision (default: state of working directory)
+    -v           verbose
+
+  Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync".
+""",
+          "A:" -> (arg => afp_root = Some(Path.explode(arg))),
+          "C" -> { _ => clean = true; dry_run = true },
+          "a:" -> (arg => afp_rev = arg),
+          "f" -> (_ => dry_run = false),
+          "n" -> (_ => dry_run = true),
+          "r:" -> (arg => rev = arg),
+          "v" -> (_ => verbose = true))
+
+        val more_args = getopts(args)
+        val target =
+          more_args match {
+            case List(target) => target
+            case _ => getopts.usage()
+          }
+
+        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)
+      }
+    )
+}
diff -r 9e34819a7ca1 -r b1748f6ca6c8 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat May 28 10:45:45 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Sun May 29 22:47:34 2022 +0200
@@ -16,7 +16,8 @@
   type Graph = isabelle.Graph[String, Unit]
 
 
-  /* HTTP server */
+
+  /** HTTP server **/
 
   object Server {
     def apply(root: String): Server = new Server(root)
@@ -79,6 +80,9 @@
   }
 
 
+
+  /** repository commands **/
+
   /* command-line syntax */
 
   def optional(s: String, prefix: String = ""): String =
@@ -132,6 +136,10 @@
     find(ssh.expand_path(start))
   }
 
+  def the_repository(start: Path, ssh: SSH.System = SSH.Local): Repository =
+    find_repository(start, ssh = ssh) getOrElse
+      error("No repository found in " + start.absolute)
+
   private def make_repository(
     root: Path,
     cmd: String,
@@ -238,8 +246,42 @@
         opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
     }
 
-    def known_files(): List[String] =
-      hg.command("status", options = "--modified --added --clean --no-status").check.out_lines
+    def status(options: String = ""): List[String] =
+      hg.command("status", options = options).check.out_lines
+
+    def known_files(): List[String] = status(options = "--modified --added --clean --no-status")
+
+    def sync(target: String,
+      progress: Progress = new Progress,
+      verbose: Boolean = false,
+      dry_run: Boolean = false,
+      clean: Boolean = false,
+      filter: List[String] = Nil,
+      rev: String = ""
+    ): Unit = {
+      require(ssh == SSH.Local, "local repository required")
+
+      Isabelle_System.with_tmp_dir("rsync") { tmp_dir =>
+        val (options, source) =
+          if (rev.isEmpty) {
+            val exclude_path = tmp_dir + Path.explode("exclude")
+            val exclude = status(options = "--unknown --ignored --no-status")
+            File.write(exclude_path, cat_lines((".hg" :: exclude).map("/" + _)))
+
+            val options = List("--exclude-from=" + exclude_path.implode)
+            val source = File.standard_path(root)
+            (options, source)
+          }
+          else {
+            val source = File.standard_path(tmp_dir + Path.explode("archive"))
+            archive(source, rev = rev)
+            (Nil, source)
+          }
+        Isabelle_System.rsync(
+          progress = progress, verbose = verbose, dry_run = dry_run, clean = clean, filter = filter,
+          args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target)).check
+      }
+    }
 
     def graph(): Graph = {
       val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
@@ -256,7 +298,8 @@
   }
 
 
-  /* check files */
+
+  /** check files **/
 
   def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) = {
     val outside = new mutable.ListBuffer[Path]
@@ -283,7 +326,8 @@
   }
 
 
-  /* setup remote vs. local repository */
+
+  /** hg_setup **/
 
   private def edit_hgrc(local_hg: Repository, path_name: String, source: String): Unit = {
     val hgrc = local_hg.root + Path.explode(".hg/hgrc")
@@ -395,7 +439,7 @@
     local_hg.push(remote = remote_url)
   }
 
-  val isabelle_tool =
+  val isabelle_tool1 =
     Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository",
       Scala_Project.here,
       { args =>
@@ -431,4 +475,61 @@
         hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name,
           remote_exists = remote_exists, progress = progress)
       })
+
+
+
+  /** hg_sync **/
+
+  val isabelle_tool2 =
+    Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory",
+      Scala_Project.here, { args =>
+        var clean = false
+        var protect: List[String] = Nil
+        var root: Option[Path] = None
+        var dry_run = false
+        var rev = ""
+        var verbose = false
+
+        val getopts = Getopts("""
+Usage: isabelle hg_sync [OPTIONS] TARGET
+
+  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
+    -R ROOT      explicit repository root directory
+                 (default: implicit from current directory)
+    -f           force changes: no dry-run
+    -n           no changes: dry-run
+    -r REV       explicit revision (default: state of working directory)
+    -v           verbose
+
+  Synchronize Mercurial repository with TARGET directory,
+  which can be local or remote (using notation of rsync).
+""",
+          "C" -> { _ => clean = true; dry_run = true },
+          "P:" -> (arg => protect = protect ::: List(arg)),
+          "R:" -> (arg => root = Some(Path.explode(arg))),
+          "f" -> (_ => dry_run = false),
+          "n" -> (_ => dry_run = true),
+          "r:" -> (arg => rev = arg),
+          "v" -> (_ => verbose = true))
+
+        val more_args = getopts(args)
+        val target =
+          more_args match {
+            case List(target) => target
+            case _ => getopts.usage()
+          }
+
+        val progress = new Console_Progress
+        val hg =
+          root match {
+            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)
+      }
+    )
 }
diff -r 9e34819a7ca1 -r b1748f6ca6c8 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sat May 28 10:45:45 2022 +0200
+++ b/src/Pure/General/ssh.scala	Sun May 29 22:47:34 2022 +0200
@@ -40,8 +40,8 @@
   val default_port = 22
   def make_port(port: Int): Int = if (port > 0) port else default_port
 
-  def port_suffix(port: Int): String =
-    if (port == default_port) "" else ":" + port
+  def port_suffix(port: Int, suffix: String = ":"): String =
+    if (port == default_port) "" else suffix + port
 
   def user_prefix(user: String): String =
     proper_string(user) match {
@@ -323,12 +323,13 @@
       new Session(new_options, session, on_close, nominal_host, nominal_user)
 
     def host: String = if (session.getHost == null) "" else session.getHost
+    def port: Int = session.getPort
 
     override def hg_url: String =
       "ssh://" + user_prefix(nominal_user) + nominal_host + "/"
 
     override def toString: String =
-      user_prefix(session.getUserName) + host + port_suffix(session.getPort) +
+      user_prefix(session.getUserName) + host + port_suffix(port) +
       (if (session.isConnected) "" else " (disconnected)")
 
 
diff -r 9e34819a7ca1 -r b1748f6ca6c8 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat May 28 10:45:45 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun May 29 22:47:34 2022 +0200
@@ -420,6 +420,25 @@
     else error("Expected to find GNU tar executable")
   }
 
+  def rsync(
+    cwd: JFile = null,
+    progress: Progress = new Progress,
+    verbose: Boolean = false,
+    dry_run: Boolean = false,
+    clean: Boolean = false,
+    filter: List[String] = Nil,
+    args: List[String] = Nil
+  ): Process_Result = {
+    val script =
+      "rsync --protect-args --archive" +
+        (if (verbose || dry_run) " --verbose" else "") +
+        (if (dry_run) " --dry-run" else "") +
+        (if (clean) " --delete-excluded" else "") +
+        filter.map(s => " --filter=" + Bash.string(s)).mkString +
+        (if (args.nonEmpty) " " + Bash.strings(args) else "")
+    progress.bash(script, cwd = cwd, echo = true)
+  }
+
   def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {
     with_tmp_file("patch") { patch =>
       Isabelle_System.bash(
diff -r 9e34819a7ca1 -r b1748f6ca6c8 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Sat May 28 10:45:45 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Sun May 29 22:47:34 2022 +0200
@@ -182,7 +182,8 @@
   Dump.isabelle_tool,
   Export.isabelle_tool,
   ML_Process.isabelle_tool,
-  Mercurial.isabelle_tool,
+  Mercurial.isabelle_tool1,
+  Mercurial.isabelle_tool2,
   Mkroot.isabelle_tool,
   Logo.isabelle_tool,
   Options.isabelle_tool,
@@ -225,6 +226,7 @@
   Build_Zipperposition.isabelle_tool,
   Check_Sources.isabelle_tool,
   Components.isabelle_tool,
+  Sync_Repos.isabelle_tool,
   isabelle.vscode.Build_VSCode.isabelle_tool,
   isabelle.vscode.Build_VSCodium.isabelle_tool1,
   isabelle.vscode.Build_VSCodium.isabelle_tool2,