# HG changeset patch
# User wenzelm
# Date 1654980921 -7200
# Node ID 197a5b3a1ea22afdd5b1d7a548421bdd30896763
# Parent  be33ca6f45d7c47b25be87ed79ac1fbe1199448c
promote "isabelle sync" to regular user-space tool, with proper documentation;

diff -r be33ca6f45d7 -r 197a5b3a1ea2 NEWS
--- a/NEWS	Sat Jun 11 20:45:14 2022 +0200
+++ b/NEWS	Sat Jun 11 22:55:21 2022 +0200
@@ -148,6 +148,13 @@
 directory of a local Mercurial repository with a target directory, using
 rsync notation for destinations.
 
+* Command-line tool "isabelle sync" synchronizes Isabelle + AFP
+repositories with a target directory, based on "isabelle hg_sync". Local
+jars and sessions images may be uploaded as well, to avoid redundant
+builds on the remote side. This tool requires a Mercurial clone of the
+Isabelle repository: a regular download of the distribution will not
+work!
+
 
 
 New in Isabelle2021-1 (December 2021)
diff -r be33ca6f45d7 -r 197a5b3a1ea2 etc/build.props
--- a/etc/build.props	Sat Jun 11 20:45:14 2022 +0200
+++ b/etc/build.props	Sat Jun 11 22:55:21 2022 +0200
@@ -38,7 +38,6 @@
   src/Pure/Admin/isabelle_devel.scala \
   src/Pure/Admin/jenkins.scala \
   src/Pure/Admin/other_isabelle.scala \
-  src/Pure/Admin/sync.scala \
   src/Pure/Concurrent/consumer_thread.scala \
   src/Pure/Concurrent/counter.scala \
   src/Pure/Concurrent/delay.scala \
@@ -189,6 +188,7 @@
   src/Pure/Tools/server_commands.scala \
   src/Pure/Tools/simplifier_trace.scala \
   src/Pure/Tools/spell_checker.scala \
+  src/Pure/Tools/sync.scala \
   src/Pure/Tools/task_statistics.scala \
   src/Pure/Tools/update.scala \
   src/Pure/Tools/update_cartouches.scala \
diff -r be33ca6f45d7 -r 197a5b3a1ea2 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Sat Jun 11 20:45:14 2022 +0200
+++ b/src/Doc/System/Misc.thy	Sat Jun 11 22:55:21 2022 +0200
@@ -300,7 +300,7 @@
 \<close>
 
 
-section \<open>Mercurial repository synchronization\<close>
+section \<open>Mercurial repository synchronization \label{sec:tool-hg-sync}\<close>
 
 text \<open>
   The @{tool_def hg_sync} tool synchronizes a local Mercurial repository with
@@ -425,6 +425,100 @@
 \<close>
 
 
+section \<open>Isabelle and AFP repository synchronization\<close>
+
+text \<open>
+  The @{tool_def sync} tool synchronizes a local Isabelle and AFP repository,
+  potentially including its prebuilt \<^verbatim>\<open>.jar\<close> files and session images.
+
+  @{verbatim [display]
+\<open>Usage: isabelle sync [OPTIONS] TARGET
+
+  Options are:
+    -A ROOT      include AFP with given root directory (":" for $AFP_BASE)
+    -H           purge heaps directory on target
+    -I NAME      include session heap image and build database
+                 (based on accidental local state)
+    -J           preserve *.jar files
+    -S           robust (but less portable) treatment of spaces in
+                 file and directory names on the target
+    -T           thorough treatment of file content and directory times
+    -a REV       explicit AFP revision (default: state of working directory)
+    -n           no changes: dry-run
+    -r REV       explicit revision (default: state of working directory)
+    -p PORT      explicit SSH port (default: 22)
+    -v           verbose
+
+  Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".\<close>}
+
+  The approach is to apply @{tool hg_sync} (\secref{sec:tool-hg-sync}) on the
+  underlying Isabelle repository plus a given AFP repository (optional). This
+  means that the Isabelle installation needs to be a Mercurial repository
+  clone: a regular download of the Isabelle distribution is not sufficient!
+
+  On the target side, AFP is placed into @{setting ISABELLE_HOME} as immediate
+  sub-directory with the literal name \<^verbatim>\<open>AFP\<close>; thus it can be easily included
+  elsewhere, e.g. @{tool build}~\<^verbatim>\<open>-d\<close>~\<^verbatim>\<open>'~~/AFP'\<close> on the remote side.
+
+  \<^medskip> Options \<^verbatim>\<open>-T\<close>, \<^verbatim>\<open>-n\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-v\<close> are the same as the underlying
+  @{tool hg_sync}.
+
+  \<^medskip> Options \<^verbatim>\<open>-r\<close> and \<^verbatim>\<open>-a\<close> are the same as option \<^verbatim>\<open>-r\<close> for @{tool hg_sync},
+  but for the Isabelle and AFP repositories, respectively. The AFP version is
+  only used if a corresponding repository is given via option \<^verbatim>\<open>-A\<close>, either
+  with explicit root directory, or as \<^verbatim>\<open>-A:\<close> to refer to \<^verbatim>\<open>$AFP_BASE\<close> (this
+  assumes AFP as component of the local Isabelle installation).
+
+  \<^medskip> Option \<^verbatim>\<open>-J\<close> uploads existing \<^verbatim>\<open>.jar\<close> files, which are usually
+  Isabelle/Scala/Java modules under control of \<^verbatim>\<open>etc/build.props\<close> (see also
+  \secref{sec:scala-build}). Normally, the underlying dependency management is
+  accurate: bad uploads will be rebuilt on the remote side (or ignored). For
+  historic Isabelle versions, going far back into the past via option \<^verbatim>\<open>-r\<close>,
+  it is better to omit option \<^verbatim>\<open>-J\<close> and thus purge \<^verbatim>\<open>.jar\<close> files on the target
+  (because they do not belong to the repository).
+
+  \<^medskip> Option \<^verbatim>\<open>-I\<close> uploads a collection of session images. The set of \<^verbatim>\<open>-I\<close>
+  options specifies the end-points in the session build graph, including all
+  required ancestors. The result collection is uploaded using the underlying
+  \<^verbatim>\<open>rsync\<close> policies: unchanged images are ignored. Session images are
+  assembled within the target \<^verbatim>\<open>heaps\<close> directory: this scheme fits together
+  with @{tool build}~\<^verbatim>\<open>-o system_heaps\<close>. Images are taken as-is from the local
+  Isabelle installation, regardless of option \<^verbatim>\<open>-r\<close>. Bad images do not cause
+  any harm, apart from wasting network bandwidth and file-system space:
+  running e.g. @{tool build} on the target will check dependencies accurately,
+  and rebuild outdated images on demand.
+
+  \<^medskip> Option \<^verbatim>\<open>-H\<close> tells the underlying \<^verbatim>\<open>rsync\<close> process to purge the \<^verbatim>\<open>heaps\<close>
+  directory on the target, before uploading new images from \<^verbatim>\<open>-I\<close> options. The
+  default is to work monotonically: old material that is not overwritten
+  remains unchanged, it is never deleted. Over time, this may lead to
+  unreachable garbage, due to changes in session names or Poly/ML versions.
+  Option \<^verbatim>\<open>-H\<close> helps to avoid wasting file-system space, although @{tool
+  build} does not require it, due to its precise checking of all dependencies.
+
+  \<^medskip> Option \<^verbatim>\<open>-S\<close> uses \<^verbatim>\<open>rsync --protect-args\<close>, but this requires at least
+  \<^verbatim>\<open>rsync 3.0.0\<close>, while many versions of macOS still ship \<^verbatim>\<open>rsync 2.9.x\<close>.
+  Since Isabelle + AFP don't use spaces or other special characters, it is
+  usually safe to omit this non-portable option.
+\<close>
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+  Quick testing of Isabelle + AFP on a remote machine: upload changed sources,
+  jars, and local sessions images for \<^verbatim>\<open>HOL\<close>:
+  @{verbatim [display] \<open>  isabelle sync -A: -I HOL -J testmachine:test/isabelle_afp\<close>}
+  Assuming that the local \<^verbatim>\<open>HOL\<close> hierarchy has been up-to-date, and the local
+  and remote ML platforms coincide, a remote @{tool build} will proceed
+  without building \<^verbatim>\<open>HOL\<close> again.
+
+  \<^medskip> A variation for accurate testing of Isabelle + AFP: no option \<^verbatim>\<open>-J\<close>, but
+  option \<^verbatim>\<open>-T\<close> to disable the default ``quick check'' of \<^verbatim>\<open>rsync\<close> (which only
+  inspects file sizes and date stamps):
+  @{verbatim [display] \<open> isabelle sync -A: -T testmachine:test/isabelle_afp\<close>}
+\<close>
+
+
 section \<open>Output the version identifier of the Isabelle distribution\<close>
 
 text \<open>
diff -r be33ca6f45d7 -r 197a5b3a1ea2 src/Pure/Admin/sync.scala
--- a/src/Pure/Admin/sync.scala	Sat Jun 11 20:45:14 2022 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,153 +0,0 @@
-/*  Title:      Pure/Admin/sync.scala
-    Author:     Makarius
-
-Synchronize Isabelle + AFP repositories.
-*/
-
-package isabelle
-
-
-object Sync {
-  /* session images */
-
-  def find_images(options: Options, session_images: List[String],
-    dirs: List[Path] = Nil
-  ): List[String] = {
-    if (session_images.isEmpty) Nil
-    else {
-      val store = Sessions.store(options)
-      val sessions_structure = Sessions.load_structure(options, dirs = dirs)
-      sessions_structure.build_requirements(session_images).flatMap { session =>
-        val heap =
-          store.find_heap(session).map(_.expand).map(path =>
-            File.standard_path(path.dir.dir) + "/./" + path.dir.file_name + "/" + path.file_name)
-        val db =
-          store.find_database(session).map(_.expand).map(path =>
-            File.standard_path(path.dir.dir.dir) + "/./" + path.dir.dir.file_name + "/" +
-              path.dir.file_name + "/" + path.file_name)
-        heap.toList ::: db.toList
-      }
-    }
-  }
-
-
-  /* sync */
-
-  def sync(options: Options, context: Rsync.Context, target: String,
-    verbose: Boolean = false,
-    thorough: Boolean = false,
-    purge_heaps: Boolean = false,
-    session_images: List[String] = Nil,
-    preserve_jars: Boolean = false,
-    dry_run: Boolean = false,
-    rev: String = "",
-    afp_root: Option[Path] = None,
-    afp_rev: String = ""
-  ): Unit = {
-    val hg = Mercurial.self_repository()
-    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,
-      contents: List[File.Content] = Nil, filter: List[String] = Nil
-    ): Unit = {
-      hg.sync(context, dest, rev = r, verbose = verbose, thorough = thorough, dry_run = dry_run,
-        contents = contents, filter = filter ::: more_filter)
-    }
-
-    context.progress.echo_if(verbose, "\n* Isabelle repository:")
-    val filter_heaps = if (purge_heaps) Nil else List("protect /heaps", "protect /heaps/**")
-    sync(hg, target, rev,
-      contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
-      filter = filter_heaps ::: List("protect /AFP"))
-
-    for (hg <- afp_hg) {
-      context.progress.echo_if(verbose, "\n* AFP repository:")
-      sync(hg, Rsync.append(target, "AFP"), afp_rev)
-    }
-
-    val images =
-      find_images(options, session_images,
-        dirs = afp_root.map(_ + Path.explode("thys")).toList)
-    if (images.nonEmpty) {
-      context.progress.echo_if(verbose, "\n* Session images:")
-      Rsync.exec(context, verbose = verbose, thorough = thorough, dry_run = dry_run,
-        args = List("--relative", "--") ::: images ::: List(Rsync.append(target, "heaps/"))).check
-    }
-  }
-
-  val isabelle_tool =
-    Isabelle_Tool("sync", "synchronize Isabelle + AFP repositories",
-      Scala_Project.here, { args =>
-        var afp_root: Option[Path] = None
-        var purge_heaps = false
-        var session_images = List.empty[String]
-        var preserve_jars = false
-        var protect_args = false
-        var thorough = false
-        var afp_rev = ""
-        var dry_run = false
-        var rev = ""
-        var port = SSH.default_port
-        var verbose = false
-
-        val getopts = Getopts("""
-Usage: isabelle sync [OPTIONS] TARGET
-
-  Options are:
-    -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
-    -H           purge heaps directory on target
-    -I NAME      include session heap image and build database
-                 (based on accidental local state)
-    -J           preserve *.jar files
-    -S           robust (but less portable) treatment of spaces in directory names
-    -T           thorough treatment of file content and directory times
-    -a REV       explicit AFP revision (default: state of working directory)
-    -n           no changes: dry-run
-    -r REV       explicit revision (default: state of working directory)
-    -p PORT      explicit SSH port (default: """ + SSH.default_port + """)
-    -v           verbose
-
-  Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync".
-
-  Example: quick testing
-
-    isabelle sync -A: -J testmachine:test/isabelle_afp
-
-  Example: accurate testing
-
-    isabelle sync -A: -T testmachine:test/isabelle_afp
-
-  Example: incremental testing based on session images
-
-    isabelle sync -A: -I HOL-Analysis testmachine:test/isabelle_afp
-""",
-          "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
-          "H" -> (_ => purge_heaps = true),
-          "I:" -> (arg => session_images = session_images ::: List(arg)),
-          "J" -> (_ => preserve_jars = true),
-          "S" -> (_ => protect_args = true),
-          "T" -> (_ => thorough = true),
-          "a:" -> (arg => afp_rev = arg),
-          "n" -> (_ => dry_run = true),
-          "r:" -> (arg => rev = arg),
-          "p:" -> (arg => port = Value.Int.parse(arg)),
-          "v" -> (_ => verbose = true))
-
-        val more_args = getopts(args)
-        val target =
-          more_args match {
-            case List(target) => target
-            case _ => getopts.usage()
-          }
-
-        val options = Options.init()
-        val progress = new Console_Progress
-        val context = Rsync.Context(progress, port = port, protect_args = protect_args)
-        sync(options, context, target, verbose = verbose, thorough = thorough,
-          purge_heaps = purge_heaps, session_images = session_images, preserve_jars = preserve_jars,
-          dry_run = dry_run, rev = rev, afp_root = afp_root, afp_rev = afp_rev)
-      }
-    )
-}
diff -r be33ca6f45d7 -r 197a5b3a1ea2 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Sat Jun 11 20:45:14 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Sat Jun 11 22:55:21 2022 +0200
@@ -195,6 +195,7 @@
   Server.isabelle_tool,
   Sessions.isabelle_tool,
   Scala_Project.isabelle_tool,
+  Sync.isabelle_tool,
   Update.isabelle_tool,
   Update_Cartouches.isabelle_tool,
   Update_Comments.isabelle_tool,
@@ -226,7 +227,6 @@
   Build_Zipperposition.isabelle_tool,
   Check_Sources.isabelle_tool,
   Components.isabelle_tool,
-  Sync.isabelle_tool,
   isabelle.vscode.Build_VSCode.isabelle_tool,
   isabelle.vscode.Build_VSCodium.isabelle_tool1,
   isabelle.vscode.Build_VSCodium.isabelle_tool2,
diff -r be33ca6f45d7 -r 197a5b3a1ea2 src/Pure/Tools/sync.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/sync.scala	Sat Jun 11 22:55:21 2022 +0200
@@ -0,0 +1,142 @@
+/*  Title:      Pure/Tools/sync.scala
+    Author:     Makarius
+
+Synchronize Isabelle + AFP repositories.
+*/
+
+package isabelle
+
+
+object Sync {
+  /* session images */
+
+  def find_images(options: Options, session_images: List[String],
+    dirs: List[Path] = Nil
+  ): List[String] = {
+    if (session_images.isEmpty) Nil
+    else {
+      val store = Sessions.store(options)
+      val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+      sessions_structure.build_requirements(session_images).flatMap { session =>
+        val heap =
+          store.find_heap(session).map(_.expand).map(path =>
+            File.standard_path(path.dir.dir) + "/./" + path.dir.file_name + "/" + path.file_name)
+        val db =
+          store.find_database(session).map(_.expand).map(path =>
+            File.standard_path(path.dir.dir.dir) + "/./" + path.dir.dir.file_name + "/" +
+              path.dir.file_name + "/" + path.file_name)
+        heap.toList ::: db.toList
+      }
+    }
+  }
+
+
+  /* sync */
+
+  def sync(options: Options, context: Rsync.Context, target: String,
+    verbose: Boolean = false,
+    thorough: Boolean = false,
+    purge_heaps: Boolean = false,
+    session_images: List[String] = Nil,
+    preserve_jars: Boolean = false,
+    dry_run: Boolean = false,
+    rev: String = "",
+    afp_root: Option[Path] = None,
+    afp_rev: String = ""
+  ): Unit = {
+    val hg = Mercurial.self_repository()
+    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,
+      contents: List[File.Content] = Nil, filter: List[String] = Nil
+    ): Unit = {
+      hg.sync(context, dest, rev = r, verbose = verbose, thorough = thorough, dry_run = dry_run,
+        contents = contents, filter = filter ::: more_filter)
+    }
+
+    context.progress.echo_if(verbose, "\n* Isabelle repository:")
+    val filter_heaps = if (purge_heaps) Nil else List("protect /heaps", "protect /heaps/**")
+    sync(hg, target, rev,
+      contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
+      filter = filter_heaps ::: List("protect /AFP"))
+
+    for (hg <- afp_hg) {
+      context.progress.echo_if(verbose, "\n* AFP repository:")
+      sync(hg, Rsync.append(target, "AFP"), afp_rev)
+    }
+
+    val images =
+      find_images(options, session_images,
+        dirs = afp_root.map(_ + Path.explode("thys")).toList)
+    if (images.nonEmpty) {
+      context.progress.echo_if(verbose, "\n* Session images:")
+      Rsync.exec(context, verbose = verbose, thorough = thorough, dry_run = dry_run,
+        args = List("--relative", "--") ::: images ::: List(Rsync.append(target, "heaps/"))).check
+    }
+  }
+
+  val isabelle_tool =
+    Isabelle_Tool("sync", "synchronize Isabelle + AFP repositories",
+      Scala_Project.here, { args =>
+        var afp_root: Option[Path] = None
+        var purge_heaps = false
+        var session_images = List.empty[String]
+        var preserve_jars = false
+        var protect_args = false
+        var thorough = false
+        var afp_rev = ""
+        var dry_run = false
+        var rev = ""
+        var port = SSH.default_port
+        var verbose = false
+
+        val getopts = Getopts("""
+Usage: isabelle sync [OPTIONS] TARGET
+
+  Options are:
+    -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
+    -H           purge heaps directory on target
+    -I NAME      include session heap image and build database
+                 (based on accidental local state)
+    -J           preserve *.jar files
+    -S           robust (but less portable) treatment of spaces in
+                 file and directory names on the target
+    -T           thorough treatment of file content and directory times
+    -a REV       explicit AFP revision (default: state of working directory)
+    -n           no changes: dry-run
+    -r REV       explicit revision (default: state of working directory)
+    -p PORT      explicit SSH port (default: """ + SSH.default_port + """)
+    -v           verbose
+
+  Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".
+""",
+          "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
+          "H" -> (_ => purge_heaps = true),
+          "I:" -> (arg => session_images = session_images ::: List(arg)),
+          "J" -> (_ => preserve_jars = true),
+          "S" -> (_ => protect_args = true),
+          "T" -> (_ => thorough = true),
+          "a:" -> (arg => afp_rev = arg),
+          "n" -> (_ => dry_run = true),
+          "r:" -> (arg => rev = arg),
+          "p:" -> (arg => port = Value.Int.parse(arg)),
+          "v" -> (_ => verbose = true))
+
+        val more_args = getopts(args)
+        val target =
+          more_args match {
+            case List(target) => target
+            case _ => getopts.usage()
+          }
+
+        val options = Options.init()
+        val progress = new Console_Progress
+        val context = Rsync.Context(progress, port = port, protect_args = protect_args)
+        sync(options, context, target, verbose = verbose, thorough = thorough,
+          purge_heaps = purge_heaps, session_images = session_images, preserve_jars = preserve_jars,
+          dry_run = dry_run, rev = rev, afp_root = afp_root, afp_rev = afp_rev)
+      }
+    )
+}