--- 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)
--- 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 \
--- 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>
--- 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)
- }
- )
-}
--- 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,
--- /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)
+ }
+ )
+}