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