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:43:31 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)
+      }
+    )
+}